Theorem eleq2i 2820

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eleq12i  2821  eleqtri  2826  eleq2s  2846  hbxfreq  2858  nfceqi  2888  raleqbii  3314  rexeqbii  3315  rabeqi  3416  rabrabi  3422  reqabi  3426  elab2gw  3642  elab2g  3644  elrabf  3652  elrab3t  3655  elrab2  3659  cbvsbcw  3783  cbvsbcvw  3784  cbvsbc  3785  elin2  4162  elsymdif  4217  noel  4297  eltpg  4646  elunirab  4882  elintrab  4920  disjxiun  5099  exss  5418  otiunsndisj  5475  brabsb  5486  brabga  5489  epelg  5532  pofun  5557  elxp  5654  opeliunxp  5698  opeliun2xp  5699  bropaex12  5722  brab2a  5724  elcnv  5830  dmopabelb  5870  elrnmptg  5914  elres  5980  elimampt  6003  elrid  6006  rninxp  6140  elid  6160  elsuci  6389  elsucg  6390  elsuc2g  6391  elfv  6838  0fv  6884  opabiota  6925  dffv2  6938  fvopab3g  6945  fvmptex  6964  fvopab5  6983  fvn0ssdmfun  7028  fveqressseq  7033  f0cli  7052  fmptco  7083  fvrnressn  7115  funfvima  7186  elunirnALT  7208  fliftel  7266  eloprabga  7478  elrnmpo  7505  elimampo  7506  ovid  7510  offval  7642  sucexeloniOLD  7766  1st2val  7975  2nd2val  7976  bropopvvv  8046  bropfvvvv  8048  fsplit  8073  xporderlem  8083  frpoins3xpg  8096  frpoins3xp3g  8097  brtpos2  8188  frrlem8  8249  frrlem9  8250  frrlem10  8251  fprresex  8266  issmo  8294  smores3  8299  tfrlem7  8328  tfrlem9  8330  tfrlem9a  8331  tfr2b  8341  tfr2  8343  rdgsuc  8369  frsucmptn  8384  tz7.48-2  8387  el1o  8436  ord2eln012  8438  dif1o  8441  ondif2  8443  oawordeulem  8495  elecg  8692  brecop  8760  erovlem  8763  eceqoveq  8772  mapsncnv  8843  mptelixpg  8885  brsdom  8923  isfi  8924  enssdom  8925  brdom2  8930  xpcomco  9008  brsdom2  9042  en3lplem2  9542  cnfcom2lem  9630  brttrcl2  9643  ttrcltr  9645  rnttrcl  9651  epfrs  9660  r1limg  9700  r1ord  9709  r1ord3  9711  tz9.12lem3  9718  rankvaln  9728  r1elss  9735  rankpwi  9752  ssrankr1  9764  r1val3  9767  r1pw  9774  rankr1b  9793  djur  9848  djuunxp  9850  eldju2ndl  9853  eldju2ndr  9854  isnum2  9874  cardprclem  9908  infxpenlem  9942  alephcard  9999  alephnbtwn  10000  alephnbtwn2  10001  alephord2  10005  alephsdom  10015  dfac3  10050  dfac5lem2  10053  dfac5lem3  10054  dfac5lem5  10056  pwsdompw  10132  cfub  10178  cardcf  10181  cflecard  10182  cfle  10183  cflim2  10192  cofsmo  10198  cfidm  10204  isfin3  10225  isfin5  10228  isfin6  10229  sdom2en01  10231  fin23lem26  10254  fin23lem30  10271  isf32lem5  10286  itunitc1  10349  ituniiun  10351  axdc3lem3  10381  axcclem  10386  axdclem  10448  iunfo  10468  iundom2g  10469  cardidg  10477  konigthlem  10497  alephadd  10506  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  elgch  10551  fpwwe2lem11  10570  canth4  10576  wunex2  10667  r1tskina  10711  elni  10805  nlt1pi  10835  adderpq  10885  mulerpq  10886  recmulnq  10893  addsrpr  11004  mulsrpr  11005  opelcn  11058  opelreal  11059  elreal  11060  elreal2  11061  0ncn  11062  addcnsr  11064  mulcnsr  11065  xrlenlt  11215  elnn0  12420  elnnne0  12432  un0addcl  12451  un0mulcl  12452  elxnn0  12493  uztrn2  12788  elnnuz  12813  elnn0uz  12814  elq  12885  elxr  13052  elfzm1b  13539  elfz0lmr  13719  uzrdgfni  13899  fzennn  13909  ser0  13995  hash2pwpr  14417  iswrd  14456  pfxccatpfx1  14677  s3iunsndisj  14910  sumz  15664  sumss  15666  fsumcvg3  15671  abscvgcvg  15761  isumshft  15781  prodf1  15833  prodeq1i  15858  zprod  15879  prod1  15886  prodss  15889  prodsn  15904  prodsnf  15906  bpolydiflem  15996  bpoly2  15999  bpoly3  16000  bpoly4  16001  ruclem6  16179  divides  16200  dvdsflip  16263  pwp1fsum  16337  sadc0  16400  eulerthlem2  16728  prm23lt5  16761  4sqlem2  16896  4sqlem12  16903  vdwpc  16927  xpscf  17504  cidpropd  17647  oppcsect  17716  funcpropd  17840  natpropd  17917  dfinito2  17941  dftermo2  17942  initoeu2lem0  17951  arwhoma  17983  eldmcoa  18003  pospo  18280  psss  18515  ismgmn0  18545  gsumpropd2lem  18582  elefmndbas  18776  smndex1basss  18808  smndex1mgm  18810  pwmnd  18840  dfgrp2e  18871  mulgfval  18977  eqg0subg  19104  cycsubmel  19108  ghmeqker  19151  elcntr  19238  cntri  19240  cntzsgrpcl  19242  oppgsubg  19271  fvcosymgeq  19335  symgfixels  19340  pmtrfrn  19364  efgsfo  19645  efgrelexlemb  19656  lt6abl  19801  dmdprd  19906  dprdval  19911  dprdw  19918  srgbinomlem4  20114  isnirred  20305  isrhm  20363  issrng  20729  lspexchn2  21017  lspindp2l  21020  lspindp2  21021  lbsextlem2  21045  rnglidl1  21118  df2idl2  21143  2idlss  21148  rngqiprngimfo  21187  cnfldfun  21254  cnfldfunOLD  21267  pzriprnglem3  21369  pzriprnglem4  21370  pzriprnglem7  21373  pzriprnglem8  21374  pzriprnglem9  21375  pzriprnglem12  21378  pzriprnglem14  21380  dsmmelbas  21624  frlmbas3  21661  lindsind2  21704  islindf4  21723  psrbagf  21803  evlslem4  21959  psdmul  22029  ply1bascl2  22065  cply1mul  22159  lply1binom  22173  matsubgcell  22297  matinvgcell  22298  matvscacell  22299  matepmcl  22325  matepm2cl  22326  scmatscm  22376  smatvscl  22387  marrepcl  22427  marepvcl  22432  mulmarep1el  22435  mulmarep1gsum1  22436  mulmarep1gsum2  22437  submabas  22441  m1detdiag  22460  mdetdiag  22462  m2detleib  22494  gsummatr01lem3  22520  gsummatr01  22522  smadiadetlem4  22532  slesolinv  22543  slesolinvbi  22544  slesolex  22545  cramerimplem2  22547  pmatcoe1fsupp  22564  mat2pmatbas  22589  mat2pmatmul  22594  mat2pmatlin  22598  decpmatmul  22635  monmatcollpw  22642  pm2mpf1  22662  pm2mpghm  22679  istps  22797  mretopd  22955  neiptopuni  22993  lpdifsn  23006  restcls  23044  perfopn  23048  pnfnei  23083  mnfnei  23084  lmss  23161  hauscmplem  23269  is2ndc  23309  2ndcdisj  23319  hausnlly  23356  txuni2  23428  ptpjpre1  23434  elpt  23435  dfac14  23481  xkococn  23523  fbasrn  23747  fin1aufil  23795  elfm2  23811  elfm3  23813  fbflim  23839  flffbas  23858  cnpflf2  23863  fclsbas  23884  efmndtmd  23964  tsmssubm  24006  iscusp2  24165  imasdsf1olem  24237  metustel  24414  metuel2  24429  isnghm  24587  opnreen  24696  iccpnfcnv  24818  ehleudisval  25295  ehl1eudis  25296  ehl2eudis  25298  minveclem3b  25304  ovoliunlem1  25379  ioombl1lem4  25438  subopnmbl  25481  vitalilem2  25486  vitalilem3  25487  mbfimaopnlem  25532  mbfimaopn2  25534  itg2l  25606  dvply1  26167  vieta1lem1  26194  vieta1lem2  26195  elaa  26200  taylthlem2  26258  taylthlem2OLD  26259  abelthlem6  26322  abelthlem9  26326  sinq34lt0t  26394  ellogrn  26444  dvrelog  26522  ellogdm  26524  logtayl2  26547  cxpcn3lem  26633  cxpcn3  26634  1cubr  26728  atandm  26762  atanf  26766  reasinsin  26782  atans2  26817  dmarea  26843  xrlimcnp  26854  amgmlem  26876  ppiublem1  27089  lgsdir2lem2  27213  gausslemma2dlem1a  27252  lgsquadlem1  27267  lgsquadlem2  27268  2sqlem1  27304  rpvmasum2  27399  madeval2  27737  newval  27739  leftval  27747  rightval  27748  lltropt  27760  madess  27764  oldssmade  27765  lrold  27784  addsproplem2  27853  addsproplem4  27855  addsproplem6  27857  negsproplem4  27913  negsproplem6  27915  precsexlem10  28094  precsexlem11  28095  sltonold  28138  elnns  28208  elzs  28248  edgiedgb  28957  isuhgr  28963  isushgr  28964  isupgr  28987  isumgr  28998  umgredg  29041  umgrpredgv  29043  umgredgne  29048  umgredgnlp  29050  isuspgr  29055  isusgr  29056  ausgrusgri  29071  usgredgppr  29099  edgssv2  29101  uspgredg2vlem  29126  uspgredg2v  29127  ushgredgedg  29132  ushgredgedgloop  29134  griedg0ssusgr  29168  uhgrissubgr  29178  subumgredg2  29188  uhgrspansubgrlem  29193  umgrres1lem  29213  upgrres1  29216  nbgrcl  29238  nbuhgr  29246  nbuhgr2vtx1edgblem  29254  nbupgrres  29267  edgnbusgreu  29270  nbusgredgeu0  29271  nbusgrf1o0  29272  hashnbusgrnn0  29279  nbupgruvtxres  29310  cffldtocusgr  29350  cffldtocusgrOLD  29351  cusgrfilem2  29360  vtxdg0v  29377  vtxduhgr0nedg  29396  uhgrvd00  29438  vtxdginducedm1  29447  finsumvtxdg2ssteplem4  29452  wlk1walk  29542  wlkp1lem6  29580  iswwlks  29739  wwlknllvtx  29749  wwlksonvtx  29758  wspthnonp  29762  wlkiswwlksupgr2  29780  wwlksnwwlksnon  29818  2pthon3v  29846  umgr2wlk  29852  elwwlks2s3  29854  wwlks2onv  29856  elwwlks2ons3im  29857  isclwwlk  29886  clwwlkccatlem  29891  clwlkclwwlk  29904  wwlksext2clwwlk  29959  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  clwwlknon1  29999  clwwlknon1nloop  30001  clwwlknon2x  30005  1pthon2v  30055  uhgr3cyclex  30084  isconngr  30091  isconngr1  30092  eucrctshift  30145  frgrnbnb  30195  frgrncvvdeqlem1  30201  frgrncvvdeqlem2  30202  frgrncvvdeqlem3  30203  frgrncvvdeqlem9  30209  fusgreghash2wspv  30237  extwwlkfab  30254  numclwwlk1lem2foa  30256  numclwwlk1lem2fo  30260  clwlknon2num  30270  numclwlk2lem2f1o  30281  numclwwlk5lem  30289  topnfbey  30371  isvclem  30479  isnvlem  30512  vsfval  30535  h2hlm  30882  hhcmpl  31102  hhcms  31105  elch0  31156  omlsilem  31304  h1de2ctlem  31457  elspansni  31460  nonbooli  31553  spansncvi  31554  adjeq  31837  cnlnssadj  31982  cnvbraval  32012  brabgaf  32509  2ndresdju  32546  fmptdF  32553  fmptcof2  32554  acunirnmpt  32556  acunirnmpt2  32557  ofpreima  32562  fcnvgreu  32570  fdifsuppconst  32585  1stpreima  32603  2ndpreima  32604  fz2ssnn0  32681  elxrge02  32825  ccatws1f1o  32846  gsumwrd2dccatlem  32979  psgnfzto1stlem  33030  cycpmgcl  33083  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem4  33169  elrgspnsubrunlem1  33171  nsgqusf1olem2  33358  nsgqusf1olem3  33359  prmidl0  33394  crngmxidl  33413  opprnsg  33428  rprmirredb  33476  zringfrac  33498  evl1deg2  33519  evl1deg3  33520  ply1degltel  33533  ply1degleel  33534  fldextrspunlsplem  33641  isconstr  33699  constrsuc  33701  constrconj  33708  submatres  33769  lmat22lem  33780  crefdf  33811  cmppcmp  33821  rspectopn  33830  prsdm  33877  prsrn  33878  xrge0iifcnv  33896  xrge0iifiso  33898  xrge0iifhom  33900  pnfneige0  33914  qqhre  33983  rrhre  33984  esumnul  34011  esumcvgsum  34051  ldgenpisyslem1  34126  measvuni  34177  cntnevol  34191  dya2iocnrect  34245  sibf0  34298  oddpwdc  34318  eulerpartlemd  34330  eulerpartgbij  34336  eulerpartlemgh  34342  isrrvv  34407  coinfliprv  34447  ballotlem7  34500  signswch  34525  hashreprin  34584  chtvalz  34593  circlemethhgt  34607  hgt750lemb  34620  tgoldbachgt  34627  bnj23  34681  bnj158  34692  bnj168  34693  bnj1138  34751  bnj1143  34753  bnj1454  34805  bnj110  34821  bnj882  34889  bnj893  34891  bnj916  34896  bnj970  34910  bnj983  34914  bnj984  34915  bnj1137  34958  bnj1174  34966  bnj1388  34996  bnj1398  34997  onvf1odlem4  35066  loop1cycl  35097  subfacp1lem5  35144  satfv1  35323  satfrnmapom  35330  satf0op  35337  satf0n0  35338  fmlafvel  35345  fmlaomn0  35350  fmlan0  35351  satffunlem2lem2  35366  satfv0fvfmla0  35373  satefvfmla0  35378  mrsub0  35476  mrsubccat  35478  mrsubcn  35479  elmrsubrn  35480  msubco  35491  msubvrs  35520  elmthm  35536  mthmblem  35540  ellcsrspsn  35601  elrn3  35722  dfon2lem7  35750  brsset  35850  eltrans  35852  elfix  35864  ellimits  35871  elfuns  35876  elsingles  35879  fvtransport  35993  brcolinear2  36019  fvray  36102  linedegen  36104  fvline  36105  ellines  36113  fwddifn0  36125  elhf  36135  hfninf  36147  rmoeqi  36148  rmoeqbii  36149  reueqi  36150  reueqbii  36151  rabeqbii  36155  iuneq12i  36156  iineq1i  36157  iineq12i  36158  riotaeqbii  36159  ixpeq1i  36161  itgeq12i  36167  cbvprodvw2  36208  fnessref  36318  bj-ififc  36543  bj-csbsnlem  36864  bj-elgab  36900  currysetlem1  36908  bj-eltag  36938  bj-sngltag  36944  bj-projun  36955  bj-velpwALT  37014  bj-0nelmpt  37077  bj-opelidres  37122  bj-inftyexpitaudisj  37166  bj-elccinfty  37175  f1omptsnlem  37297  icoreelrnab  37315  relowlpssretop  37325  rdgssun  37339  exrecfnlem  37340  finxpnom  37362  uncov  37568  tan2h  37579  ptrecube  37587  poimirlem25  37612  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  cnambfre  37635  ftc1cnnc  37659  sdclem2  37709  sdclem1  37710  fdc  37712  caushft  37728  issmgrpOLD  37830  ismndo  37839  isrngo  37864  isdivrngo  37917  csbcom2fi  38095  elecALTV  38228  brrabga  38296  eldmxrncnvepres  38369  eldmxrncnvepres2  38370  eldmcoss  38422  coss0  38443  elrels2  38450  dath  39703  diclspsn  41161  dvh4dimlem  41410  dvh2dim  41412  dvh3dim3N  41416  lcfrvalsnN  41508  mapdh6eN  41707  mapdh7dN  41717  mapdh8b  41747  hdmap1l6e  41781  lcmfunnnd  41973  3factsumint1  41982  primrootsunit1  42058  primrootscoprmpow  42060  aks6d1c2lem4  42088  sticksstones2  42108  sticksstones3  42109  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  aks6d1c6lem2  42132  aks6d1c6lem3  42133  redvmptabs  42321  readvrec2  42322  readvrec  42323  frlmfielbas  42461  mhpind  42555  pellex  42796  rmspecnonsq  42868  islmodfg  43031  aaitgo  43124  areaquad  43178  ordeldif1o  43222  naddwordnexlem4  43363  fpwfvss  43374  finona1cl  43415  elcnvcnvintab  43544  elnonrel  43547  elcnvcnvlem  43561  cnvcnvintabd  43562  brfvrcld2  43654  grur1cld  44194  dvgrat  44274  cvgdvgrat  44275  radcnvrat  44276  nznngen  44278  uzmptshftfval  44308  binomcxplemcvg  44316  binomcxplemnotnn0  44318  tpid3gVD  44804  en3lplem2VD  44806  orbitclmpt  44921  wfaxrep  44957  wfaxsep  44958  wfaxpow  44960  wfaxpr  44961  wfaxun  44962  wfac8prim  44965  brpermmodelcnv  44967  nregmodellem  44979  iuneq1i  45052  rexanuz3  45063  eliuniin  45066  eliuniin2  45087  disjinfi  45159  fsneq  45173  iuneqfzuzlem  45303  allbutfi  45362  eluzelz2  45372  uz0  45381  uzublem  45399  uzid3  45404  elicores  45504  uzinico  45530  climsuselem1  45578  climsuse  45579  islptre  45590  fnlimfvre  45645  limsupresico  45671  limsupvaluz  45679  limsupubuzlem  45683  limsupequzmptlem  45699  liminfresico  45742  cnrefiisplem  45800  stoweidlem14  45985  stoweidlem39  46010  stoweidlem48  46019  stoweidlem51  46022  stoweidlem59  46030  stoweidlem62  46033  wallispilem3  46038  fourierdlem42  46120  fourierdlem62  46139  fourierdlem80  46157  fourierdlem103  46180  fourierdlem104  46181  etransclem26  46231  rrxsnicc  46271  ioorrnopn  46276  ioorrnopnxr  46278  sge00  46347  sge0fodjrnlem  46387  sge0isum  46398  sge0seq  46417  meadjiunlem  46436  carageneld  46473  volicorescl  46524  hoidmv1lelem1  46562  hoidmv1le  46565  hoidmvlelem1  46566  hoidmvlelem3  46568  ovnhoilem2  46573  hoiqssbllem2  46594  opnvonmbllem2  46604  ovolval4lem1  46620  iinhoiicc  46645  vonioolem1  46651  smflimlem1  46742  smflimlem2  46743  smflim  46748  nsssmfmbf  46750  smfresal  46759  smfrec  46760  smfdiv  46768  smfpimbor1lem2  46770  smflim2  46777  smflimmpt  46781  smfinflem  46788  smflimsuplem1  46791  smflimsuplem2  46792  smflimsuplem3  46793  smflimsuplem5  46795  smflimsuplem6  46796  smflimsup  46799  smflimsupmpt  46800  smfliminfmpt  46803  tannpoly  46864  sinnpoly  46865  fcores  47041  ndmaovcl  47177  ndmaovcom  47179  ndmaovass  47180  ndmaovdistr  47181  dfatco  47230  otiunsndisjX  47253  fvmptrabdm  47267  ceilhalfelfzo1  47304  modmknepk  47336  elsetpreimafvb  47358  sprsymrelfolem2  47467  sprsymrelf  47469  sprsymrelf1  47470  prpair  47475  prproropf1olem0  47476  paireqne  47485  fmtno4prmfac  47546  dfodd5  47634  sbgoldbo  47761  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  clnbgrcl  47795  clnbgredg  47813  sclnbgrel  47820  isubgredg  47839  uhgrimedgi  47863  isuspgrim0  47867  isuspgrimlem  47868  gricushgr  47890  clnbgrgrimlem  47906  grimedg  47908  usgrgrtrirex  47922  stgrnbgr0  47936  isubgr3stgrlem3  47940  isubgr3stgrlem4  47941  isubgr3stgrlem6  47943  isubgr3stgrlem7  47944  uspgrlimlem2  47961  uspgrlimlem3  47962  grlimgrtrilem1  47966  grlimgrtrilem2  47967  usgrexmpl2trifr  48001  gpgvtxel  48011  gpgedgel  48014  gpgusgralem  48020  gpg5order  48024  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgnbgrvtx0  48038  gpgnbgrvtx1  48039  gpg5nbgrvtx03star  48044  gpg5nbgr3star  48045  gpgvtxdg3  48046  gpg5gricstgr3  48054  gpgprismgr4cycllem3  48060  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem8  48065  gpgprismgr4cycllem10  48067  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  pgnbgreunbgr  48088  uspgrsprf  48107  uspgrsprf1  48108  uspgrsprfo  48109  ply1sclrmsm  48345  lcoop  48373  lincfsuppcl  48375  linccl  48376  lincvalsng  48378  lincvalpr  48380  lincvalsc0  48383  linc0scn0  48385  lincdifsn  48386  linc1  48387  lincsum  48391  lincscm  48392  lspsslco  48399  snlindsntor  48433  lincresunit3lem2  48442  ldepsnlinclem1  48467  ldepsnlinclem2  48468  prelrrx2  48675  prelrrx2b  48676  rrx2xpref1o  48680  rrx2plord  48682  rrx2linesl  48705  sectrcl  48984  invrcl  48986  initopropdlemlem  49201  initopropd  49205  termopropd  49206  zeroopropd  49207  oppcthin  49400  indthinc  49424  prsthinc  49426  elpglem3  49675