Theorem eleq2i 2884

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 2881	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 197   = wceq 1637   ∈ wcel 2157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2806  df-clel 2809

This theorem is referenced by:  eleq12i  2885  eleqtri  2890  eleq2s  2910  hbxfreq  2921  raleqbii  3185  rexeqbii  3249  rabeq2i  3394  elab2g  3555  elrabf  3562  elrab3t  3565  elrab2  3569  cbvsbc  3669  elin2  4007  elsymdif  4054  dfnul2  4125  noel  4127  eltpg  4426  elunirab  4649  elintrab  4688  disjxiun  4848  exss  5128  otiunsndisj  5182  brabsb  5188  brabga  5191  pofun  5255  elxp  5340  opeliunxp  5377  bropaex12  5401  brab2a  5403  elcnv  5507  elrnmptg  5583  opelresg  5610  opelresOLD  5614  elres  5645  elrid  5669  elid  5671  rninxp  5791  elsuci  6010  elsucg  6011  elsuc2g  6012  elfv  6409  0fv  6450  opabiota  6485  dffv2  6495  fvopab3g  6501  fvmptex  6518  fvopab5  6534  fvn0ssdmfun  6575  fveqressseq  6580  f0cli  6595  fmptco  6622  fvrnressn  6655  funfvima  6720  elunirnALT  6737  fliftel  6786  eloprabga  6980  elrnmpt2  7006  ovid  7010  offval  7137  suceloni  7246  1st2val  7429  2nd2val  7430  bropopvvv  7492  bropfvvvv  7494  fsplit  7519  xporderlem  7525  brtpos2  7596  wfrdmcl  7662  wfrfun  7664  wfrlem12  7665  wfrlem17  7670  wfr2  7673  issmo  7684  smores3  7689  tfrlem7  7718  tfrlem9  7720  tfrlem9a  7721  tfr2b  7731  tfr2  7733  rdgsuc  7759  frsucmptn  7773  tz7.48-2  7776  el1o  7819  dif1o  7820  ondif2  7822  oawordeulem  7874  elecg  8023  brecop  8078  erovlem  8082  eceqoveq  8091  mapsncnv  8144  mptelixpg  8185  brsdom  8218  isfi  8219  enssdom  8220  brdom2  8225  xpcomco  8292  brsdom2  8326  en3lplem2  8758  cnfcom2lem  8848  epfrs  8857  r1limg  8884  r1ord  8893  r1ord3  8895  tz9.12lem3  8902  rankvaln  8912  r1elss  8919  rankpwi  8936  ssrankr1  8948  r1val3  8951  r1pw  8958  rankr1b  8977  djur  9031  djuunxp  9033  eldju2ndl  9036  eldju2ndr  9037  isnum2  9057  cardprclem  9091  infxpenlem  9122  alephcard  9179  alephnbtwn  9180  alephnbtwn2  9181  alephord2  9185  alephsdom  9195  dfac3  9230  dfac5lem2  9233  dfac5lem3  9234  dfac5lem5  9236  pwsdompw  9314  cfub  9359  cardcf  9362  cflecard  9363  cfle  9364  cflim2  9373  cofsmo  9379  cfidm  9385  isfin3  9406  isfin5  9409  isfin6  9410  sdom2en01  9412  fin23lem26  9435  fin23lem30  9452  isf32lem5  9467  itunitc1  9530  ituniiun  9532  axdc3lem3  9562  axcclem  9567  axdclem  9629  iunfo  9649  iundom2g  9650  cardidg  9658  konigthlem  9678  alephadd  9687  alephreg  9692  pwcfsdom  9693  cfpwsdom  9694  elgch  9732  fpwwe2lem12  9751  canth4  9757  wunex2  9848  r1tskina  9892  elni  9986  nlt1pi  10016  adderpq  10066  mulerpq  10067  recmulnq  10074  addsrpr  10184  mulsrpr  10185  opelcn  10238  opelreal  10239  elreal  10240  elreal2  10241  0ncn  10242  addcnsr  10244  mulcnsr  10245  xrlenlt  10391  elnn0  11564  elnnne0  11576  un0addcl  11595  un0mulcl  11596  elxnn0  11634  uztrn2  11925  elnnuz  11945  elnn0uz  11946  elq  12012  elxr  12169  elfzm1b  12644  elfz0lmr  12810  uzrdgfni  12984  fzennn  12994  ser0  13079  hash2pwpr  13478  iswrd  13521  s3iunsndisj  13935  sumz  14679  sumss  14681  fsumcvg3  14686  abscvgcvg  14776  isumshft  14796  prodf1  14847  zprod  14891  prod1  14898  prodss  14901  prodsn  14916  prodsnf  14918  bpolydiflem  15008  bpoly2  15011  bpoly3  15012  bpoly4  15013  ruclem6  15187  divides  15208  dvdsflip  15265  pwp1fsum  15337  sadc0  15398  eulerthlem2  15707  prm23lt5  15739  4sqlem2  15873  4sqlem12  15880  vdwpc  15904  xpscf  16434  cidpropd  16577  oppcsect  16645  funcpropd  16767  natpropd  16843  initoeu2lem0  16870  arwhoma  16902  eldmcoa  16922  pospo  17181  psss  17422  ismgmn0  17452  gsumpropd2lem  17481  dfgrp2e  17656  ghmeqker  17892  cntri  17967  oppgsubg  17997  fvcosymgeq  18053  symgfixels  18058  pmtrfrn  18082  efgsfo  18356  efgrelexlemb  18367  lt6abl  18500  dmdprd  18602  dprdval  18607  dprdw  18614  srgbinomlem4  18748  isnirred  18905  isrhm  18928  issrng  19057  lspexchn2  19342  lspindp2l  19345  lspindp2  19346  lbsextlem2  19371  evlslem4  19719  ply1bascl2  19785  cply1mul  19875  lply1binom  19887  cnfldfunALT  19970  dsmmelbas  20297  frlmbas3  20329  lindsind2  20372  islindf4  20391  matsubgcell  20454  matinvgcell  20455  matvscacell  20456  matepmcl  20483  matepm2cl  20484  scmatscm  20534  smatvscl  20545  marrepcl  20585  marepvcl  20590  mulmarep1el  20593  mulmarep1gsum1  20594  mulmarep1gsum2  20595  submabas  20599  m1detdiag  20618  mdetdiag  20620  m2detleib  20652  gsummatr01lem3  20679  gsummatr01  20681  smadiadetlem4  20691  slesolinv  20702  slesolinvbi  20703  slesolex  20704  cramerimplem2  20707  pmatcoe1fsupp  20723  mat2pmatbas  20748  mat2pmatmul  20753  mat2pmatlin  20757  decpmatmul  20794  monmatcollpw  20801  pm2mpf1  20821  pm2mpghm  20838  istps  20956  mretopd  21114  neiptopuni  21152  lpdifsn  21165  restcls  21203  perfopn  21207  pnfnei  21242  mnfnei  21243  lmss  21320  hauscmplem  21427  is2ndc  21467  2ndcdisj  21477  hausnlly  21514  txuni2  21586  ptpjpre1  21592  elpt  21593  dfac14  21639  xkococn  21681  fbasrn  21905  fin1aufil  21953  elfm2  21969  elfm3  21971  fbflim  21997  flffbas  22016  cnpflf2  22021  fclsbas  22042  tsmssubm  22163  iscusp2  22323  imasdsf1olem  22395  metustel  22572  metuel2  22587  isnghm  22744  opnreen  22851  iccpnfcnv  22960  cvsi  23146  minveclem3b  23417  ovoliunlem1  23489  ioombl1lem4  23548  subopnmbl  23591  vitalilem2  23596  vitalilem3  23597  mbfimaopnlem  23642  mbfimaopn2  23644  itg2l  23716  dvply1  24259  vieta1lem1  24285  vieta1lem2  24286  elaa  24291  taylthlem2  24348  abelthlem6  24410  abelthlem9  24414  sinq34lt0t  24482  ellogrn  24526  dvrelog  24603  ellogdm  24605  logtayl2  24628  cxpcn3lem  24708  cxpcn3  24709  1cubr  24789  atandm  24823  atanf  24827  reasinsin  24843  atans2  24878  dmarea  24904  xrlimcnp  24915  amgmlem  24936  ppiublem1  25147  lgsdir2lem2  25271  gausslemma2dlem1a  25310  lgsquadlem1  25325  lgsquadlem2  25326  2sqlem1  25362  rpvmasum2  25421  eleenn  25996  edgiedgb  26167  isuhgr  26175  isushgr  26176  isupgr  26199  isumgr  26210  umgredg  26254  umgrpredgv  26256  umgredgne  26261  umgredgnlp  26263  isuspgr  26268  isusgr  26269  ausgrusgri  26284  usgredgppr  26309  edgssv2  26311  uspgredg2vlem  26336  uspgredg2v  26337  ushgredgedg  26342  ushgredgedgloop  26344  ushgredgedgloopOLD  26345  griedg0ssusgr  26379  uhgrissubgr  26389  subumgredg2  26399  uhgrspansubgrlem  26404  umgrres1lem  26424  upgrres1  26427  nbgrcl  26449  nbgrclOLD  26450  nbuhgr  26461  nbuhgr2vtx1edgblem  26469  nbupgrres  26487  edgnbusgreu  26490  edgnbusgreuOLD  26491  nbusgredgeu0  26492  nbusgrf1o0  26493  hashnbusgrnn0  26500  nbupgruvtxres  26536  cffldtocusgr  26577  cusgrfilem2  26586  vtxdg0v  26603  vtxduhgr0nedg  26622  uhgrvd00  26664  vtxdginducedm1  26673  finsumvtxdg2ssteplem4  26678  rgrx0ndm  26723  wlk1walk  26769  wlkp1lem6  26809  iswwlks  26963  wwlknllvtx  26974  wwlksonvtx  26984  wspthnonp  26992  wwlksn0  26996  wlkiswwlksupgr2  27010  wlknwwlksnsurOLD  27023  wwlksnwwlksnon  27059  wwlksnwwlksnonOLD  27061  2pthon3v  27089  umgr2wlk  27095  elwwlks2s3  27097  wwlks2onv  27099  elwwlks2ons3im  27100  elwwlks2ons3OLD  27102  isclwwlk  27133  clwwlkccatlem  27138  clwlkclwwlk  27151  wwlksext2clwwlk  27213  wwlksext2clwwlkOLD  27214  hashecclwwlkn1  27234  umgrhashecclwwlk  27235  clwlksfclwwlkOLD  27242  clwwlknon1  27271  clwwlknon1nloop  27273  clwwlknon2x  27277  s2elclwwlknon2  27278  1pthon2v  27332  uhgr3cyclex  27361  isconngr  27368  isconngr1  27369  eucrctshift  27422  isfrgr  27439  frgrnbnb  27474  frgrncvvdeqlem1  27480  frgrncvvdeqlem2  27481  frgrncvvdeqlem3  27482  frgrncvvdeqlem9  27488  fusgreghash2wspv  27516  extwwlkfab  27537  numclwwlk1lem2foa  27539  numclwwlk1lem2fo  27543  clwlknon2num  27554  numclwlk2lem2f1o  27565  numclwlk2lem2f1oOLD  27572  numclwwlk5lem  27581  topnfbey  27662  isvclem  27766  isnvlem  27799  vsfval  27822  h2hlm  28171  hhcmpl  28391  hhcms  28394  elch0  28445  omlsilem  28595  h1de2ctlem  28748  elspansni  28751  nonbooli  28844  spansncvi  28845  adjeq  29128  cnlnssadj  29273  cnvbraval  29303  brabgaf  29751  elimampt  29771  fmptdF  29789  fmptcof2  29790  acunirnmpt  29792  acunirnmpt2  29793  ofpreima  29798  fcnvgreu  29805  1stpreima  29817  2ndpreima  29818  fz2ssnn0  29880  elxrge02  29971  psgnfzto1stlem  30181  submatres  30203  lmat22lem  30214  crefdf  30246  cmppcmp  30256  prsdm  30291  prsrn  30292  xrge0iifcnv  30310  xrge0iifiso  30312  xrge0iifhom  30314  pnfneige0  30328  qqhre  30395  rrhre  30396  esumnul  30441  esumcvgsum  30481  ldgenpisyslem1  30557  measvuni  30608  cntnevol  30622  dya2iocnrect  30674  sibf0  30727  oddpwdc  30747  eulerpartlemd  30759  eulerpartgbij  30765  eulerpartlemgh  30771  isrrvv  30836  coinfliprv  30875  ballotlem7  30928  signswch  30969  hashreprin  31029  chtvalz  31038  circlemethhgt  31052  hgt750lemb  31065  tgoldbachgt  31072  bnj23  31115  bnj158  31126  bnj168  31127  bnj1138  31187  bnj1143  31189  bnj1454  31240  bnj110  31256  bnj882  31324  bnj893  31326  bnj916  31331  bnj970  31345  bnj983  31349  bnj984  31350  bnj1137  31391  bnj1174  31399  bnj1388  31429  bnj1398  31430  subfacp1lem5  31494  mrsub0  31741  mrsubccat  31743  mrsubcn  31744  elmrsubrn  31745  msubco  31756  msubvrs  31785  elmthm  31801  mthmblem  31805  elrn3  31979  dfon2lem7  32019  eltrpred  32051  frrlem5e  32114  frrlem11  32118  madeval2  32262  brsset  32322  eltrans  32324  elfix  32336  ellimits  32343  elfuns  32348  elsingles  32351  fvtransport  32465  brcolinear2  32491  fvray  32574  linedegen  32576  fvline  32577  ellines  32585  fwddifn0  32597  elhf  32607  hfninf  32619  fnessref  32678  bj-csbsnlem  33208  bj-sels  33262  bj-eltag  33277  bj-sngltag  33283  bj-projun  33294  bj-0nelmpt  33382  bj-elid  33403  bj-elccinfty  33420  f1omptsnlem  33502  icoreelrnab  33520  relowlpssretop  33530  finxpnom  33556  uncov  33705  tan2h  33716  ptrecube  33724  poimirlem25  33749  poimirlem29  33753  poimirlem30  33754  poimirlem31  33755  poimirlem32  33756  cnambfre  33772  ftc1cnnc  33798  sdclem2  33851  sdclem1  33852  fdc  33854  caushft  33870  issmgrpOLD  33975  ismndo  33984  isrngo  34009  isdivrngo  34062  csbcom2fi  34246  elecALTV  34350  eldmcoss  34523  coss0  34544  elrels2  34551  dath  35518  diclspsn  36976  dvh4dimlem  37225  dvh2dim  37227  dvh3dim3N  37231  lcfrvalsnN  37323  mapdh6eN  37522  mapdh7dN  37532  mapdh8b  37562  hdmap1l6e  37596  pellex  37902  rmspecnonsq  37974  islmodfg  38141  aaitgo  38234  areaquad  38303  elcnvcnvintab  38389  elnonrel  38392  elcnvcnvlem  38406  cnvcnvintabd  38407  brfvrcld2  38485  dvgrat  39012  cvgdvgrat  39013  radcnvrat  39014  nznngen  39016  uzmptshftfval  39046  binomcxplemcvg  39054  binomcxplemnotnn0  39056  tpid3gVD  39572  en3lplem2VD  39574  rexanuz3  39769  eliuniin  39773  eliuniin2  39796  disjinfi  39870  fsneq  39886  iuneqfzuzlem  40031  allbutfi  40096  eluzelz2  40107  uz0  40119  uzublem  40137  uzid3  40142  elicores  40241  uzinico  40268  climsuselem1  40320  climsuse  40321  islptre  40332  fnlimfvre  40387  limsupresico  40413  limsupvaluz  40421  limsupubuzlem  40425  limsupequzmptlem  40441  liminfresico  40484  cnrefiisplem  40536  stoweidlem14  40711  stoweidlem39  40736  stoweidlem48  40745  stoweidlem51  40748  stoweidlem59  40756  stoweidlem62  40759  wallispilem3  40764  fourierdlem42  40846  fourierdlem62  40865  fourierdlem80  40883  fourierdlem103  40906  fourierdlem104  40907  etransclem26  40957  rrxsnicc  41000  ioorrnopn  41005  ioorrnopnxr  41007  sge00  41073  sge0fodjrnlem  41113  sge0isum  41124  sge0seq  41143  ismea  41148  meadjiunlem  41162  carageneld  41199  volicorescl  41250  hoidmv1lelem1  41288  hoidmv1le  41291  hoidmvlelem1  41292  hoidmvlelem3  41294  ovnhoilem2  41299  hoiqssbllem2  41320  opnvonmbllem2  41330  ovolval4lem1  41346  iinhoiicc  41371  vonioolem1  41377  smflimlem1  41462  smflimlem2  41463  smflim  41468  nsssmfmbf  41470  smfresal  41478  smfrec  41479  smfdiv  41487  smfpimbor1lem2  41489  smflim2  41495  smflimmpt  41499  smfsupmpt  41504  smfinflem  41506  smfinfmpt  41508  smflimsuplem1  41509  smflimsuplem2  41510  smflimsuplem3  41511  smflimsuplem5  41513  smflimsuplem6  41514  smflimsup  41517  smflimsupmpt  41518  smfliminfmpt  41521  ndmaovcl  41793  ndmaovcom  41795  ndmaovass  41796  ndmaovdistr  41797  dfatco  41846  otiunsndisjX  41870  fvmptrabdm  41884  pfxccatpfx1  42003  fmtno4prmfac  42060  dfodd5  42148  sbgoldbo  42251  nnsum4primeseven  42264  nnsum4primesevenALTV  42265  sprsymrelfolem2  42312  sprsymrelf  42314  sprsymrelf1  42315  uspgrsprf  42323  uspgrsprf1  42324  uspgrsprfo  42325  opeliun2xp  42680  ply1sclrmsm  42740  lcoop  42769  lincfsuppcl  42771  linccl  42772  lincvalsng  42774  lincvalpr  42776  lincvalsc0  42779  linc0scn0  42781  lincdifsn  42782  linc1  42783  lincsum  42787  lincscm  42788  lspsslco  42795  snlindsntor  42829  lincresunit3lem2  42838  ldepsnlinclem1  42863  ldepsnlinclem2  42864  elpglem3  43028