Theorem eleq2i 2829

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

Syntax hints:   ↔ wb 205   = wceq 1540   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2729  df-clel 2815

This theorem is referenced by:  eleq12i  2830  eleqtri  2836  eleq2s  2856  hbxfreq  2868  nfceqi  2902  raleqbii  3312  rexeqbii  3313  rabeqi  3416  rabrabi  3424  rabeq2i  3426  elab2g  3621  elrabf  3630  elrab3t  3633  elrab2  3637  cbvsbcw  3760  cbvsbcvw  3761  cbvsbc  3762  elin2  4142  elsymdif  4192  noel  4275  noelOLD  4276  eltpg  4631  elunirab  4866  elintrab  4904  disjxiun  5084  exss  5397  otiunsndisj  5453  brabsb  5464  brabga  5467  epelg  5514  pofun  5539  elxp  5630  opeliunxp  5672  bropaex12  5696  brab2a  5698  elcnv  5805  dmopabelb  5845  elrnmptg  5887  elres  5949  elrid  5972  rninxp  6104  elid  6124  elsuci  6354  elsucg  6355  elsuc2g  6356  elfv  6809  0fv  6852  opabiota  6890  dffv2  6902  fvopab3g  6909  fvmptex  6928  fvopab5  6946  fvn0ssdmfun  6991  fveqressseq  6996  f0cli  7013  fmptco  7040  fvrnressn  7072  funfvima  7145  elunirnALT  7164  fliftel  7219  eloprabga  7422  eloprabgaOLD  7423  elrnmpo  7450  ovid  7454  offval  7582  sucexeloniOLD  7700  suceloniOLD  7702  1st2val  7904  2nd2val  7905  bropopvvv  7975  bropfvvvv  7977  fsplit  8002  xporderlem  8012  brtpos2  8095  frrlem8  8156  frrlem9  8157  frrlem10  8158  fprresex  8173  wfrdmclOLD  8195  wfrfunOLD  8197  wfrlem12OLD  8198  wfrlem17OLD  8203  wfr2OLD  8206  issmo  8226  smores3  8231  tfrlem7  8261  tfrlem9  8263  tfrlem9a  8264  tfr2b  8274  tfr2  8276  rdgsuc  8302  frsucmptn  8317  tz7.48-2  8320  el1o  8373  ord2eln012  8375  dif1o  8378  ondif2  8380  oawordeulem  8433  elecg  8589  brecop  8647  erovlem  8650  eceqoveq  8659  mapsncnv  8729  mptelixpg  8771  brsdom  8813  isfi  8814  enssdom  8815  brdom2  8820  xpcomco  8904  brsdom2  8939  en3lplem2  9442  cnfcom2lem  9530  brttrcl2  9543  ttrcltr  9545  rnttrcl  9551  epfrs  9560  r1limg  9600  r1ord  9609  r1ord3  9611  tz9.12lem3  9618  rankvaln  9628  r1elss  9635  rankpwi  9652  ssrankr1  9664  r1val3  9667  r1pw  9674  rankr1b  9693  djur  9748  djuunxp  9750  eldju2ndl  9753  eldju2ndr  9754  isnum2  9774  cardprclem  9808  infxpenlem  9842  alephcard  9899  alephnbtwn  9900  alephnbtwn2  9901  alephord2  9905  alephsdom  9915  dfac3  9950  dfac5lem2  9953  dfac5lem3  9954  dfac5lem5  9956  pwsdompw  10033  cfub  10078  cardcf  10081  cflecard  10082  cfle  10083  cflim2  10092  cofsmo  10098  cfidm  10104  isfin3  10125  isfin5  10128  isfin6  10129  sdom2en01  10131  fin23lem26  10154  fin23lem30  10171  isf32lem5  10186  itunitc1  10249  ituniiun  10251  axdc3lem3  10281  axcclem  10286  axdclem  10348  iunfo  10368  iundom2g  10369  cardidg  10377  konigthlem  10397  alephadd  10406  alephreg  10411  pwcfsdom  10412  cfpwsdom  10413  elgch  10451  fpwwe2lem11  10470  canth4  10476  wunex2  10567  r1tskina  10611  elni  10705  nlt1pi  10735  adderpq  10785  mulerpq  10786  recmulnq  10793  addsrpr  10904  mulsrpr  10905  opelcn  10958  opelreal  10959  elreal  10960  elreal2  10961  0ncn  10962  addcnsr  10964  mulcnsr  10965  xrlenlt  11113  elnn0  12308  elnnne0  12320  un0addcl  12339  un0mulcl  12340  elxnn0  12380  uztrn2  12674  elnnuz  12695  elnn0uz  12696  elq  12763  elxr  12925  elfzm1b  13407  elfz0lmr  13575  uzrdgfni  13751  fzennn  13761  ser0  13848  hash2pwpr  14262  iswrd  14291  pfxccatpfx1  14521  s3iunsndisj  14751  sumz  15506  sumss  15508  fsumcvg3  15513  abscvgcvg  15603  isumshft  15623  prodf1  15675  zprod  15719  prod1  15726  prodss  15729  prodsn  15744  prodsnf  15746  bpolydiflem  15836  bpoly2  15839  bpoly3  15840  bpoly4  15841  ruclem6  16016  divides  16037  dvdsflip  16098  pwp1fsum  16172  sadc0  16233  eulerthlem2  16553  prm23lt5  16585  4sqlem2  16720  4sqlem12  16727  vdwpc  16751  xpscf  17346  cidpropd  17489  oppcsect  17560  funcpropd  17686  natpropd  17764  dfinito2  17788  dftermo2  17789  initoeu2lem0  17798  arwhoma  17830  eldmcoa  17850  pospo  18133  psss  18368  ismgmn0  18398  gsumpropd2lem  18433  elefmndbas  18581  smndex1basss  18613  smndex1mgm  18615  pwmnd  18645  dfgrp2e  18674  mulgfval  18771  cycsubmel  18888  ghmeqker  18930  cntri  19006  oppgsubg  19039  fvcosymgeq  19106  symgfixels  19111  pmtrfrn  19135  efgsfo  19413  efgrelexlemb  19424  lt6abl  19564  dmdprd  19669  dprdval  19674  dprdw  19681  srgbinomlem4  19847  isnirred  20010  isrhm  20033  issrng  20182  lspexchn2  20465  lspindp2l  20468  lspindp2  20469  lbsextlem2  20493  cnfldfun  20681  dsmmelbas  21018  frlmbas3  21055  lindsind2  21098  islindf4  21117  psrbagf  21193  evlslem4  21356  ply1bascl2  21447  cply1mul  21537  lply1binom  21549  matsubgcell  21655  matinvgcell  21656  matvscacell  21657  matepmcl  21683  matepm2cl  21684  scmatscm  21734  smatvscl  21745  marrepcl  21785  marepvcl  21790  mulmarep1el  21793  mulmarep1gsum1  21794  mulmarep1gsum2  21795  submabas  21799  m1detdiag  21818  mdetdiag  21820  m2detleib  21852  gsummatr01lem3  21878  gsummatr01  21880  smadiadetlem4  21890  slesolinv  21901  slesolinvbi  21902  slesolex  21903  cramerimplem2  21905  pmatcoe1fsupp  21922  mat2pmatbas  21947  mat2pmatmul  21952  mat2pmatlin  21956  decpmatmul  21993  monmatcollpw  22000  pm2mpf1  22020  pm2mpghm  22037  istps  22155  mretopd  22315  neiptopuni  22353  lpdifsn  22366  restcls  22404  perfopn  22408  pnfnei  22443  mnfnei  22444  lmss  22521  hauscmplem  22629  is2ndc  22669  2ndcdisj  22679  hausnlly  22716  txuni2  22788  ptpjpre1  22794  elpt  22795  dfac14  22841  xkococn  22883  fbasrn  23107  fin1aufil  23155  elfm2  23171  elfm3  23173  fbflim  23199  flffbas  23218  cnpflf2  23223  fclsbas  23244  efmndtmd  23324  tsmssubm  23366  iscusp2  23526  imasdsf1olem  23598  metustel  23778  metuel2  23793  isnghm  23959  opnreen  24066  iccpnfcnv  24179  ehleudisval  24655  ehl1eudis  24656  ehl2eudis  24658  minveclem3b  24664  ovoliunlem1  24738  ioombl1lem4  24797  subopnmbl  24840  vitalilem2  24845  vitalilem3  24846  mbfimaopnlem  24891  mbfimaopn2  24893  itg2l  24966  dvply1  25516  vieta1lem1  25542  vieta1lem2  25543  elaa  25548  taylthlem2  25605  abelthlem6  25667  abelthlem9  25671  sinq34lt0t  25738  ellogrn  25787  dvrelog  25864  ellogdm  25866  logtayl2  25889  cxpcn3lem  25972  cxpcn3  25973  1cubr  26064  atandm  26098  atanf  26102  reasinsin  26118  atans2  26153  dmarea  26179  xrlimcnp  26190  amgmlem  26211  ppiublem1  26422  lgsdir2lem2  26546  gausslemma2dlem1a  26585  lgsquadlem1  26600  lgsquadlem2  26601  2sqlem1  26637  rpvmasum2  26732  edgiedgb  27533  isuhgr  27539  isushgr  27540  isupgr  27563  isumgr  27574  umgredg  27617  umgrpredgv  27619  umgredgne  27624  umgredgnlp  27626  isuspgr  27631  isusgr  27632  ausgrusgri  27647  usgredgppr  27672  edgssv2  27674  uspgredg2vlem  27699  uspgredg2v  27700  ushgredgedg  27705  ushgredgedgloop  27707  griedg0ssusgr  27741  uhgrissubgr  27751  subumgredg2  27761  uhgrspansubgrlem  27766  umgrres1lem  27786  upgrres1  27789  nbgrcl  27811  nbuhgr  27819  nbuhgr2vtx1edgblem  27827  nbupgrres  27840  edgnbusgreu  27843  nbusgredgeu0  27844  nbusgrf1o0  27845  hashnbusgrnn0  27852  nbupgruvtxres  27883  cffldtocusgr  27923  cusgrfilem2  27932  vtxdg0v  27949  vtxduhgr0nedg  27968  uhgrvd00  28010  vtxdginducedm1  28019  finsumvtxdg2ssteplem4  28024  wlk1walk  28115  wlkp1lem6  28155  iswwlks  28310  wwlknllvtx  28320  wwlksonvtx  28329  wspthnonp  28333  wlkiswwlksupgr2  28351  wwlksnwwlksnon  28389  2pthon3v  28417  umgr2wlk  28423  elwwlks2s3  28425  wwlks2onv  28427  elwwlks2ons3im  28428  isclwwlk  28457  clwwlkccatlem  28462  clwlkclwwlk  28475  wwlksext2clwwlk  28530  hashecclwwlkn1  28550  umgrhashecclwwlk  28551  clwwlknon1  28570  clwwlknon1nloop  28572  clwwlknon2x  28576  1pthon2v  28626  uhgr3cyclex  28655  isconngr  28662  isconngr1  28663  eucrctshift  28716  frgrnbnb  28766  frgrncvvdeqlem1  28772  frgrncvvdeqlem2  28773  frgrncvvdeqlem3  28774  frgrncvvdeqlem9  28780  fusgreghash2wspv  28808  extwwlkfab  28825  numclwwlk1lem2foa  28827  numclwwlk1lem2fo  28831  clwlknon2num  28841  numclwlk2lem2f1o  28852  numclwwlk5lem  28860  topnfbey  28942  isvclem  29048  isnvlem  29081  vsfval  29104  h2hlm  29451  hhcmpl  29671  hhcms  29674  elch0  29725  omlsilem  29873  h1de2ctlem  30026  elspansni  30029  nonbooli  30122  spansncvi  30123  adjeq  30406  cnlnssadj  30551  cnvbraval  30581  brabgaf  31056  elimampt  31081  2ndresdju  31094  fmptdF  31101  fmptcof2  31102  acunirnmpt  31104  acunirnmpt2  31105  ofpreima  31110  fcnvgreu  31118  fdifsuppconst  31131  1stpreima  31147  2ndpreima  31148  fz2ssnn0  31214  elxrge02  31314  psgnfzto1stlem  31475  cycpmgcl  31528  nsgqusf1olem2  31704  nsgqusf1olem3  31705  prmidl0  31731  submatres  31862  lmat22lem  31873  crefdf  31904  cmppcmp  31914  rspectopn  31923  prsdm  31970  prsrn  31971  xrge0iifcnv  31989  xrge0iifiso  31991  xrge0iifhom  31993  pnfneige0  32007  qqhre  32076  rrhre  32077  esumnul  32122  esumcvgsum  32162  ldgenpisyslem1  32237  measvuni  32288  cntnevol  32302  dya2iocnrect  32354  sibf0  32407  oddpwdc  32427  eulerpartlemd  32439  eulerpartgbij  32445  eulerpartlemgh  32451  isrrvv  32516  coinfliprv  32555  ballotlem7  32608  signswch  32646  hashreprin  32706  chtvalz  32715  circlemethhgt  32729  hgt750lemb  32742  tgoldbachgt  32749  bnj23  32803  bnj158  32814  bnj168  32815  bnj1138  32873  bnj1143  32875  bnj1454  32927  bnj110  32943  bnj882  33011  bnj893  33013  bnj916  33018  bnj970  33032  bnj983  33036  bnj984  33037  bnj1137  33080  bnj1174  33088  bnj1388  33118  bnj1398  33119  loop1cycl  33204  subfacp1lem5  33251  satfv1  33430  satfrnmapom  33437  satf0op  33444  satf0n0  33445  fmlafvel  33452  fmlaomn0  33457  fmlan0  33458  satffunlem2lem2  33473  satfv0fvfmla0  33480  satefvfmla0  33485  mrsub0  33583  mrsubccat  33585  mrsubcn  33586  elmrsubrn  33587  msubco  33598  msubvrs  33627  elmthm  33643  mthmblem  33647  elrn3  33829  dfon2lem7  33864  frpoins3xpg  33885  frpoins3xp3g  33886  madeval2  34095  newval  34097  leftval  34105  rightval  34106  madess  34117  oldssmade  34118  lrold  34135  brsset  34249  eltrans  34251  elfix  34263  ellimits  34270  elfuns  34275  elsingles  34278  fvtransport  34392  brcolinear2  34418  fvray  34501  linedegen  34503  fvline  34504  ellines  34512  fwddifn0  34524  elhf  34534  hfninf  34546  fnessref  34604  bj-ififc  34821  bj-csbsnlem  35145  bj-elgab  35184  currysetlem1  35193  bj-eltag  35223  bj-sngltag  35229  bj-projun  35240  bj-0nelmpt  35343  bj-opelidres  35388  bj-inftyexpitaudisj  35432  bj-elccinfty  35441  f1omptsnlem  35563  icoreelrnab  35581  relowlpssretop  35591  rdgssun  35605  exrecfnlem  35606  finxpnom  35628  uncov  35814  tan2h  35825  ptrecube  35833  poimirlem25  35858  poimirlem29  35862  poimirlem30  35863  poimirlem31  35864  poimirlem32  35865  cnambfre  35881  ftc1cnnc  35905  sdclem2  35956  sdclem1  35957  fdc  35959  caushft  35975  issmgrpOLD  36077  ismndo  36086  isrngo  36111  isdivrngo  36164  csbcom2fi  36342  elecALTV  36482  brrabga  36558  eldmcoss  36676  coss0  36697  elrels2  36704  dath  37955  diclspsn  39413  dvh4dimlem  39662  dvh2dim  39664  dvh3dim3N  39668  lcfrvalsnN  39760  mapdh6eN  39959  mapdh7dN  39969  mapdh8b  39999  hdmap1l6e  40033  lcmfunnnd  40225  3factsumint1  40234  sticksstones2  40311  sticksstones3  40312  sticksstones10  40319  sticksstones12a  40321  sticksstones12  40322  elab2gw  40374  frlmfielbas  40434  mhpind  40486  prjcrv0  40673  pellex  40860  rmspecnonsq  40932  islmodfg  41098  aaitgo  41191  areaquad  41251  finona1cl  41281  elcnvcnvintab  41411  elnonrel  41414  elcnvcnvlem  41428  cnvcnvintabd  41429  brfvrcld2  41521  grur1cld  42071  dvgrat  42151  cvgdvgrat  42152  radcnvrat  42153  nznngen  42155  uzmptshftfval  42185  binomcxplemcvg  42193  binomcxplemnotnn0  42195  tpid3gVD  42683  en3lplem2VD  42685  rexanuz3  42867  eliuniin  42870  eliuniin2  42891  disjinfi  42959  fsneq  42974  iuneqfzuzlem  43109  allbutfi  43169  eluzelz2  43179  uz0  43188  uzublem  43206  uzid3  43211  elicores  43308  uzinico  43335  climsuselem1  43385  climsuse  43386  islptre  43397  fnlimfvre  43452  limsupresico  43478  limsupvaluz  43486  limsupubuzlem  43490  limsupequzmptlem  43506  liminfresico  43549  cnrefiisplem  43607  stoweidlem14  43792  stoweidlem39  43817  stoweidlem48  43826  stoweidlem51  43829  stoweidlem59  43837  stoweidlem62  43840  wallispilem3  43845  fourierdlem42  43927  fourierdlem62  43946  fourierdlem80  43964  fourierdlem103  43987  fourierdlem104  43988  etransclem26  44038  rrxsnicc  44078  ioorrnopn  44083  ioorrnopnxr  44085  sge00  44152  sge0fodjrnlem  44192  sge0isum  44203  sge0seq  44222  meadjiunlem  44241  carageneld  44278  volicorescl  44329  hoidmv1lelem1  44367  hoidmv1le  44370  hoidmvlelem1  44371  hoidmvlelem3  44373  ovnhoilem2  44378  hoiqssbllem2  44399  opnvonmbllem2  44409  ovolval4lem1  44425  iinhoiicc  44450  vonioolem1  44456  smflimlem1  44547  smflimlem2  44548  smflim  44553  nsssmfmbf  44555  smfresal  44564  smfrec  44565  smfdiv  44573  smfpimbor1lem2  44575  smflim2  44582  smflimmpt  44586  smfinflem  44593  smfinfmpt  44595  smflimsuplem1  44596  smflimsuplem2  44597  smflimsuplem3  44598  smflimsuplem5  44600  smflimsuplem6  44601  smflimsup  44604  smflimsupmpt  44605  smfliminfmpt  44608  fcores  44813  ndmaovcl  44947  ndmaovcom  44949  ndmaovass  44950  ndmaovdistr  44951  dfatco  45000  otiunsndisjX  45023  fvmptrabdm  45037  elsetpreimafvb  45088  sprsymrelfolem2  45197  sprsymrelf  45199  sprsymrelf1  45200  prpair  45205  prproropf1olem0  45206  paireqne  45215  fmtno4prmfac  45276  dfodd5  45364  sbgoldbo  45491  nnsum4primeseven  45504  nnsum4primesevenALTV  45505  isomushgr  45530  isomuspgrlem2c  45534  uspgrsprf  45560  uspgrsprf1  45561  uspgrsprfo  45562  opeliun2xp  45920  ply1sclrmsm  45976  lcoop  46004  lincfsuppcl  46006  linccl  46007  lincvalsng  46009  lincvalpr  46011  lincvalsc0  46014  linc0scn0  46016  lincdifsn  46017  linc1  46018  lincsum  46022  lincscm  46023  lspsslco  46030  snlindsntor  46064  lincresunit3lem2  46073  ldepsnlinclem1  46098  ldepsnlinclem2  46099  prelrrx2  46311  prelrrx2b  46312  rrx2xpref1o  46316  rrx2plord  46318  rrx2linesl  46341  oppcthin  46572  indthinc  46585  prsthinc  46587  elpglem3  46670