Theorem eleq2i 2821

Description: Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq2i	⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq2 2818	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806

This theorem is referenced by:  eleq12i  2822  eleqtri  2827  eleq2s  2847  hbxfreq  2860  nfceqi  2896  raleqbii  3334  rexeqbii  3335  rabeqi  3441  rabrabi  3446  reqabi  3450  elab2g  3668  elrabf  3677  elrab3t  3680  elrab2  3684  cbvsbcw  3809  cbvsbcvw  3810  cbvsbc  3811  elin2  4194  elsymdif  4244  noel  4327  noelOLD  4328  eltpg  4686  elunirab  4919  elintrab  4959  disjxiun  5140  exss  5460  otiunsndisj  5517  brabsb  5528  brabga  5531  epelg  5578  pofun  5603  elxp  5696  opeliunxp  5740  bropaex12  5764  brab2a  5766  elcnv  5874  dmopabelb  5914  elrnmptg  5956  elres  6019  elrid  6044  rninxp  6178  elid  6198  elsuci  6431  elsucg  6432  elsuc2g  6433  elfv  6890  0fv  6936  opabiota  6976  dffv2  6988  fvopab3g  6995  fvmptex  7014  fvopab5  7033  fvn0ssdmfun  7079  fveqressseq  7084  f0cli  7103  fmptco  7133  fvrnressn  7165  funfvima  7237  elunirnALT  7257  fliftel  7312  eloprabga  7523  eloprabgaOLD  7524  elrnmpo  7552  elimampo  7553  ovid  7557  offval  7689  sucexeloniOLD  7808  suceloniOLD  7810  1st2val  8016  2nd2val  8017  bropopvvv  8090  bropfvvvv  8092  fsplit  8117  xporderlem  8127  frpoins3xpg  8140  frpoins3xp3g  8141  brtpos2  8232  frrlem8  8293  frrlem9  8294  frrlem10  8295  fprresex  8310  wfrdmclOLD  8332  wfrfunOLD  8334  wfrlem12OLD  8335  wfrlem17OLD  8340  wfr2OLD  8343  issmo  8363  smores3  8368  tfrlem7  8398  tfrlem9  8400  tfrlem9a  8401  tfr2b  8411  tfr2  8413  rdgsuc  8439  frsucmptn  8454  tz7.48-2  8457  el1o  8510  ord2eln012  8512  dif1o  8515  ondif2  8517  oawordeulem  8569  elecg  8762  brecop  8823  erovlem  8826  eceqoveq  8835  mapsncnv  8906  mptelixpg  8948  brsdom  8990  isfi  8991  enssdom  8992  brdom2  8997  xpcomco  9081  brsdom2  9116  en3lplem2  9631  cnfcom2lem  9719  brttrcl2  9732  ttrcltr  9734  rnttrcl  9740  epfrs  9749  r1limg  9789  r1ord  9798  r1ord3  9800  tz9.12lem3  9807  rankvaln  9817  r1elss  9824  rankpwi  9841  ssrankr1  9853  r1val3  9856  r1pw  9863  rankr1b  9882  djur  9937  djuunxp  9939  eldju2ndl  9942  eldju2ndr  9943  isnum2  9963  cardprclem  9997  infxpenlem  10031  alephcard  10088  alephnbtwn  10089  alephnbtwn2  10090  alephord2  10094  alephsdom  10104  dfac3  10139  dfac5lem2  10142  dfac5lem3  10143  dfac5lem5  10145  pwsdompw  10222  cfub  10267  cardcf  10270  cflecard  10271  cfle  10272  cflim2  10281  cofsmo  10287  cfidm  10293  isfin3  10314  isfin5  10317  isfin6  10318  sdom2en01  10320  fin23lem26  10343  fin23lem30  10360  isf32lem5  10375  itunitc1  10438  ituniiun  10440  axdc3lem3  10470  axcclem  10475  axdclem  10537  iunfo  10557  iundom2g  10558  cardidg  10566  konigthlem  10586  alephadd  10595  alephreg  10600  pwcfsdom  10601  cfpwsdom  10602  elgch  10640  fpwwe2lem11  10659  canth4  10665  wunex2  10756  r1tskina  10800  elni  10894  nlt1pi  10924  adderpq  10974  mulerpq  10975  recmulnq  10982  addsrpr  11093  mulsrpr  11094  opelcn  11147  opelreal  11148  elreal  11149  elreal2  11150  0ncn  11151  addcnsr  11153  mulcnsr  11154  xrlenlt  11304  elnn0  12499  elnnne0  12511  un0addcl  12530  un0mulcl  12531  elxnn0  12571  uztrn2  12866  elnnuz  12891  elnn0uz  12892  elq  12959  elxr  13123  elfzm1b  13606  elfz0lmr  13774  uzrdgfni  13950  fzennn  13960  ser0  14046  hash2pwpr  14464  iswrd  14493  pfxccatpfx1  14713  s3iunsndisj  14942  sumz  15695  sumss  15697  fsumcvg3  15702  abscvgcvg  15792  isumshft  15812  prodf1  15864  zprod  15908  prod1  15915  prodss  15918  prodsn  15933  prodsnf  15935  bpolydiflem  16025  bpoly2  16028  bpoly3  16029  bpoly4  16030  ruclem6  16206  divides  16227  dvdsflip  16288  pwp1fsum  16362  sadc0  16423  eulerthlem2  16745  prm23lt5  16777  4sqlem2  16912  4sqlem12  16919  vdwpc  16943  xpscf  17541  cidpropd  17684  oppcsect  17755  funcpropd  17883  natpropd  17962  dfinito2  17986  dftermo2  17987  initoeu2lem0  17996  arwhoma  18028  eldmcoa  18048  pospo  18331  psss  18566  ismgmn0  18596  gsumpropd2lem  18633  elefmndbas  18819  smndex1basss  18851  smndex1mgm  18853  pwmnd  18883  dfgrp2e  18914  mulgfval  19019  eqg0subg  19145  cycsubmel  19149  ghmeqker  19191  elcntr  19275  cntri  19277  cntzsgrpcl  19279  oppgsubg  19311  fvcosymgeq  19378  symgfixels  19383  pmtrfrn  19407  efgsfo  19688  efgrelexlemb  19699  lt6abl  19844  dmdprd  19949  dprdval  19954  dprdw  19961  srgbinomlem4  20163  isnirred  20353  isrhm  20411  issrng  20724  lspexchn2  21013  lspindp2l  21016  lspindp2  21017  lbsextlem2  21041  rnglidl1  21122  df2idl2  21145  2idlss  21150  rngqiprngimfo  21185  cnfldfun  21287  cnfldfunOLD  21300  pzriprnglem3  21403  pzriprnglem4  21404  pzriprnglem7  21407  pzriprnglem8  21408  pzriprnglem9  21409  pzriprnglem12  21412  pzriprnglem14  21414  dsmmelbas  21667  frlmbas3  21704  lindsind2  21747  islindf4  21766  psrbagf  21845  evlslem4  22014  psdmul  22084  ply1bascl2  22117  cply1mul  22209  lply1binom  22223  matsubgcell  22330  matinvgcell  22331  matvscacell  22332  matepmcl  22358  matepm2cl  22359  scmatscm  22409  smatvscl  22420  marrepcl  22460  marepvcl  22465  mulmarep1el  22468  mulmarep1gsum1  22469  mulmarep1gsum2  22470  submabas  22474  m1detdiag  22493  mdetdiag  22495  m2detleib  22527  gsummatr01lem3  22553  gsummatr01  22555  smadiadetlem4  22565  slesolinv  22576  slesolinvbi  22577  slesolex  22578  cramerimplem2  22580  pmatcoe1fsupp  22597  mat2pmatbas  22622  mat2pmatmul  22627  mat2pmatlin  22631  decpmatmul  22668  monmatcollpw  22675  pm2mpf1  22695  pm2mpghm  22712  istps  22830  mretopd  22990  neiptopuni  23028  lpdifsn  23041  restcls  23079  perfopn  23083  pnfnei  23118  mnfnei  23119  lmss  23196  hauscmplem  23304  is2ndc  23344  2ndcdisj  23354  hausnlly  23391  txuni2  23463  ptpjpre1  23469  elpt  23470  dfac14  23516  xkococn  23558  fbasrn  23782  fin1aufil  23830  elfm2  23846  elfm3  23848  fbflim  23874  flffbas  23893  cnpflf2  23898  fclsbas  23919  efmndtmd  23999  tsmssubm  24041  iscusp2  24201  imasdsf1olem  24273  metustel  24453  metuel2  24468  isnghm  24634  opnreen  24741  iccpnfcnv  24863  ehleudisval  25341  ehl1eudis  25342  ehl2eudis  25344  minveclem3b  25350  ovoliunlem1  25425  ioombl1lem4  25484  subopnmbl  25527  vitalilem2  25532  vitalilem3  25533  mbfimaopnlem  25578  mbfimaopn2  25580  itg2l  25653  dvply1  26212  vieta1lem1  26239  vieta1lem2  26240  elaa  26245  taylthlem2  26303  taylthlem2OLD  26304  abelthlem6  26367  abelthlem9  26371  sinq34lt0t  26438  ellogrn  26487  dvrelog  26565  ellogdm  26567  logtayl2  26590  cxpcn3lem  26676  cxpcn3  26677  1cubr  26768  atandm  26802  atanf  26806  reasinsin  26822  atans2  26857  dmarea  26883  xrlimcnp  26894  amgmlem  26916  ppiublem1  27129  lgsdir2lem2  27253  gausslemma2dlem1a  27292  lgsquadlem1  27307  lgsquadlem2  27308  2sqlem1  27344  rpvmasum2  27439  madeval2  27774  newval  27776  leftval  27784  rightval  27785  lltropt  27793  madess  27797  oldssmade  27798  lrold  27817  addsproplem2  27881  addsproplem4  27883  addsproplem6  27885  negsproplem4  27937  negsproplem6  27939  precsexlem10  28108  precsexlem11  28109  sltonold  28147  elnns  28202  edgiedgb  28861  isuhgr  28867  isushgr  28868  isupgr  28891  isumgr  28902  umgredg  28945  umgrpredgv  28947  umgredgne  28952  umgredgnlp  28954  isuspgr  28959  isusgr  28960  ausgrusgri  28975  usgredgppr  29003  edgssv2  29005  uspgredg2vlem  29030  uspgredg2v  29031  ushgredgedg  29036  ushgredgedgloop  29038  griedg0ssusgr  29072  uhgrissubgr  29082  subumgredg2  29092  uhgrspansubgrlem  29097  umgrres1lem  29117  upgrres1  29120  nbgrcl  29142  nbuhgr  29150  nbuhgr2vtx1edgblem  29158  nbupgrres  29171  edgnbusgreu  29174  nbusgredgeu0  29175  nbusgrf1o0  29176  hashnbusgrnn0  29183  nbupgruvtxres  29214  cffldtocusgr  29254  cffldtocusgrOLD  29255  cusgrfilem2  29264  vtxdg0v  29281  vtxduhgr0nedg  29300  uhgrvd00  29342  vtxdginducedm1  29351  finsumvtxdg2ssteplem4  29356  wlk1walk  29447  wlkp1lem6  29486  iswwlks  29641  wwlknllvtx  29651  wwlksonvtx  29660  wspthnonp  29664  wlkiswwlksupgr2  29682  wwlksnwwlksnon  29720  2pthon3v  29748  umgr2wlk  29754  elwwlks2s3  29756  wwlks2onv  29758  elwwlks2ons3im  29759  isclwwlk  29788  clwwlkccatlem  29793  clwlkclwwlk  29806  wwlksext2clwwlk  29861  hashecclwwlkn1  29881  umgrhashecclwwlk  29882  clwwlknon1  29901  clwwlknon1nloop  29903  clwwlknon2x  29907  1pthon2v  29957  uhgr3cyclex  29986  isconngr  29993  isconngr1  29994  eucrctshift  30047  frgrnbnb  30097  frgrncvvdeqlem1  30103  frgrncvvdeqlem2  30104  frgrncvvdeqlem3  30105  frgrncvvdeqlem9  30111  fusgreghash2wspv  30139  extwwlkfab  30156  numclwwlk1lem2foa  30158  numclwwlk1lem2fo  30162  clwlknon2num  30172  numclwlk2lem2f1o  30183  numclwwlk5lem  30191  topnfbey  30273  isvclem  30381  isnvlem  30414  vsfval  30437  h2hlm  30784  hhcmpl  31004  hhcms  31007  elch0  31058  omlsilem  31206  h1de2ctlem  31359  elspansni  31362  nonbooli  31455  spansncvi  31456  adjeq  31739  cnlnssadj  31884  cnvbraval  31914  brabgaf  32392  elimampt  32417  2ndresdju  32429  fmptdF  32436  fmptcof2  32437  acunirnmpt  32439  acunirnmpt2  32440  ofpreima  32445  fcnvgreu  32453  fdifsuppconst  32464  1stpreima  32481  2ndpreima  32482  fz2ssnn0  32548  elxrge02  32650  psgnfzto1stlem  32816  cycpmgcl  32869  zringfrac  32991  nsgqusf1olem2  33119  nsgqusf1olem3  33120  prmidl0  33161  crngmxidl  33177  opprnsg  33190  ply1degltel  33256  ply1degleel  33257  submatres  33402  lmat22lem  33413  crefdf  33444  cmppcmp  33454  rspectopn  33463  prsdm  33510  prsrn  33511  xrge0iifcnv  33529  xrge0iifiso  33531  xrge0iifhom  33533  pnfneige0  33547  qqhre  33616  rrhre  33617  esumnul  33662  esumcvgsum  33702  ldgenpisyslem1  33777  measvuni  33828  cntnevol  33842  dya2iocnrect  33896  sibf0  33949  oddpwdc  33969  eulerpartlemd  33981  eulerpartgbij  33987  eulerpartlemgh  33993  isrrvv  34058  coinfliprv  34097  ballotlem7  34150  signswch  34188  hashreprin  34247  chtvalz  34256  circlemethhgt  34270  hgt750lemb  34283  tgoldbachgt  34290  bnj23  34344  bnj158  34355  bnj168  34356  bnj1138  34414  bnj1143  34416  bnj1454  34468  bnj110  34484  bnj882  34552  bnj893  34554  bnj916  34559  bnj970  34573  bnj983  34577  bnj984  34578  bnj1137  34621  bnj1174  34629  bnj1388  34659  bnj1398  34660  loop1cycl  34742  subfacp1lem5  34789  satfv1  34968  satfrnmapom  34975  satf0op  34982  satf0n0  34983  fmlafvel  34990  fmlaomn0  34995  fmlan0  34996  satffunlem2lem2  35011  satfv0fvfmla0  35018  satefvfmla0  35023  mrsub0  35121  mrsubccat  35123  mrsubcn  35124  elmrsubrn  35125  msubco  35136  msubvrs  35165  elmthm  35181  mthmblem  35185  elrn3  35351  dfon2lem7  35380  brsset  35480  eltrans  35482  elfix  35494  ellimits  35501  elfuns  35506  elsingles  35509  fvtransport  35623  brcolinear2  35649  fvray  35732  linedegen  35734  fvline  35735  ellines  35743  fwddifn0  35755  elhf  35765  hfninf  35777  fnessref  35836  bj-ififc  36053  bj-csbsnlem  36376  bj-elgab  36412  currysetlem1  36421  bj-eltag  36451  bj-sngltag  36457  bj-projun  36468  bj-velpwALT  36527  bj-0nelmpt  36590  bj-opelidres  36635  bj-inftyexpitaudisj  36679  bj-elccinfty  36688  f1omptsnlem  36810  icoreelrnab  36828  relowlpssretop  36838  rdgssun  36852  exrecfnlem  36853  finxpnom  36875  uncov  37069  tan2h  37080  ptrecube  37088  poimirlem25  37113  poimirlem29  37117  poimirlem30  37118  poimirlem31  37119  poimirlem32  37120  cnambfre  37136  ftc1cnnc  37160  sdclem2  37210  sdclem1  37211  fdc  37213  caushft  37229  issmgrpOLD  37331  ismndo  37340  isrngo  37365  isdivrngo  37418  csbcom2fi  37596  elecALTV  37733  brrabga  37808  eldmcoss  37925  coss0  37946  elrels2  37953  dath  39204  diclspsn  40662  dvh4dimlem  40911  dvh2dim  40913  dvh3dim3N  40917  lcfrvalsnN  41009  mapdh6eN  41208  mapdh7dN  41218  mapdh8b  41248  hdmap1l6e  41282  lcmfunnnd  41478  3factsumint1  41487  primrootsunit1  41562  primrootscoprmpow  41565  aks6d1c2lem4  41593  sticksstones2  41614  sticksstones3  41615  sticksstones10  41622  sticksstones12a  41624  sticksstones12  41625  aks6d1c6lem2  41638  aks6d1c6lem3  41639  frlmfielbas  41731  mhpind  41818  elab2gw  42082  pellex  42246  rmspecnonsq  42318  islmodfg  42484  aaitgo  42577  areaquad  42635  ordeldif1o  42680  naddwordnexlem4  42822  fpwfvss  42833  finona1cl  42874  elcnvcnvintab  43003  elnonrel  43006  elcnvcnvlem  43020  cnvcnvintabd  43021  brfvrcld2  43113  grur1cld  43660  dvgrat  43740  cvgdvgrat  43741  radcnvrat  43742  nznngen  43744  uzmptshftfval  43774  binomcxplemcvg  43782  binomcxplemnotnn0  43784  tpid3gVD  44272  en3lplem2VD  44274  rexanuz3  44453  eliuniin  44456  eliuniin2  44477  disjinfi  44556  fsneq  44570  iuneqfzuzlem  44707  allbutfi  44766  eluzelz2  44776  uz0  44785  uzublem  44803  uzid3  44808  elicores  44909  uzinico  44936  climsuselem1  44986  climsuse  44987  islptre  44998  fnlimfvre  45053  limsupresico  45079  limsupvaluz  45087  limsupubuzlem  45091  limsupequzmptlem  45107  liminfresico  45150  cnrefiisplem  45208  stoweidlem14  45393  stoweidlem39  45418  stoweidlem48  45427  stoweidlem51  45430  stoweidlem59  45438  stoweidlem62  45441  wallispilem3  45446  fourierdlem42  45528  fourierdlem62  45547  fourierdlem80  45565  fourierdlem103  45588  fourierdlem104  45589  etransclem26  45639  rrxsnicc  45679  ioorrnopn  45684  ioorrnopnxr  45686  sge00  45755  sge0fodjrnlem  45795  sge0isum  45806  sge0seq  45825  meadjiunlem  45844  carageneld  45881  volicorescl  45932  hoidmv1lelem1  45970  hoidmv1le  45973  hoidmvlelem1  45974  hoidmvlelem3  45976  ovnhoilem2  45981  hoiqssbllem2  46002  opnvonmbllem2  46012  ovolval4lem1  46028  iinhoiicc  46053  vonioolem1  46059  smflimlem1  46150  smflimlem2  46151  smflim  46156  nsssmfmbf  46158  smfresal  46167  smfrec  46168  smfdiv  46176  smfpimbor1lem2  46178  smflim2  46185  smflimmpt  46189  smfinflem  46196  smfinfmpt  46198  smflimsuplem1  46199  smflimsuplem2  46200  smflimsuplem3  46201  smflimsuplem5  46203  smflimsuplem6  46204  smflimsup  46207  smflimsupmpt  46208  smfliminfmpt  46211  fcores  46440  ndmaovcl  46574  ndmaovcom  46576  ndmaovass  46577  ndmaovdistr  46578  dfatco  46627  otiunsndisjX  46650  fvmptrabdm  46664  elsetpreimafvb  46715  sprsymrelfolem2  46824  sprsymrelf  46826  sprsymrelf1  46827  prpair  46832  prproropf1olem0  46833  paireqne  46842  fmtno4prmfac  46903  dfodd5  46991  sbgoldbo  47118  nnsum4primeseven  47131  nnsum4primesevenALTV  47132  isuspgrim0  47161  isuspgrimlem  47163  gricushgr  47174  uspgrsprf  47199  uspgrsprf1  47200  uspgrsprfo  47201  opeliun2xp  47387  ply1sclrmsm  47442  lcoop  47470  lincfsuppcl  47472  linccl  47473  lincvalsng  47475  lincvalpr  47477  lincvalsc0  47480  linc0scn0  47482  lincdifsn  47483  linc1  47484  lincsum  47488  lincscm  47489  lspsslco  47496  snlindsntor  47530  lincresunit3lem2  47539  ldepsnlinclem1  47564  ldepsnlinclem2  47565  prelrrx2  47777  prelrrx2b  47778  rrx2xpref1o  47782  rrx2plord  47784  rrx2linesl  47807  oppcthin  48036  indthinc  48049  prsthinc  48051  elpglem3  48135

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »