Theorem eleq2i 2817

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

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802

This theorem is referenced by:  eleq12i  2818  eleqtri  2823  eleq2s  2843  hbxfreq  2856  nfceqi  2888  raleqbii  3327  rexeqbii  3328  rabeqi  3432  rabrabi  3437  reqabi  3441  elab2g  3666  elrabf  3675  elrab3t  3678  elrab2  3682  cbvsbcw  3807  cbvsbcvw  3808  cbvsbc  3809  elin2  4195  elsymdif  4246  noel  4330  noelOLD  4331  eltpg  4691  elunirab  4924  elintrab  4964  disjxiun  5146  exss  5465  otiunsndisj  5522  brabsb  5533  brabga  5536  epelg  5583  pofun  5608  elxp  5701  opeliunxp  5745  bropaex12  5769  brab2a  5771  elcnv  5879  dmopabelb  5919  elrnmptg  5961  elres  6025  elrid  6050  rninxp  6185  elid  6205  elsuci  6438  elsucg  6439  elsuc2g  6440  elfv  6894  0fv  6940  opabiota  6980  dffv2  6992  fvopab3g  6999  fvmptex  7018  fvopab5  7037  fvn0ssdmfun  7083  fveqressseq  7088  f0cli  7107  fmptco  7138  fvrnressn  7170  funfvima  7242  elunirnALT  7262  fliftel  7316  eloprabga  7528  eloprabgaOLD  7529  elrnmpo  7557  elimampo  7558  ovid  7562  offval  7694  sucexeloniOLD  7814  suceloniOLD  7816  1st2val  8022  2nd2val  8023  bropopvvv  8095  bropfvvvv  8097  fsplit  8122  xporderlem  8132  frpoins3xpg  8145  frpoins3xp3g  8146  brtpos2  8238  frrlem8  8299  frrlem9  8300  frrlem10  8301  fprresex  8316  wfrdmclOLD  8338  wfrfunOLD  8340  wfrlem12OLD  8341  wfrlem17OLD  8346  wfr2OLD  8349  issmo  8369  smores3  8374  tfrlem7  8404  tfrlem9  8406  tfrlem9a  8407  tfr2b  8417  tfr2  8419  rdgsuc  8445  frsucmptn  8460  tz7.48-2  8463  el1o  8516  ord2eln012  8518  dif1o  8521  ondif2  8523  oawordeulem  8575  elecg  8768  brecop  8829  erovlem  8832  eceqoveq  8841  mapsncnv  8912  mptelixpg  8954  brsdom  8996  isfi  8997  enssdom  8998  brdom2  9003  xpcomco  9087  brsdom2  9122  en3lplem2  9638  cnfcom2lem  9726  brttrcl2  9739  ttrcltr  9741  rnttrcl  9747  epfrs  9756  r1limg  9796  r1ord  9805  r1ord3  9807  tz9.12lem3  9814  rankvaln  9824  r1elss  9831  rankpwi  9848  ssrankr1  9860  r1val3  9863  r1pw  9870  rankr1b  9889  djur  9944  djuunxp  9946  eldju2ndl  9949  eldju2ndr  9950  isnum2  9970  cardprclem  10004  infxpenlem  10038  alephcard  10095  alephnbtwn  10096  alephnbtwn2  10097  alephord2  10101  alephsdom  10111  dfac3  10146  dfac5lem2  10149  dfac5lem3  10150  dfac5lem5  10152  pwsdompw  10229  cfub  10274  cardcf  10277  cflecard  10278  cfle  10279  cflim2  10288  cofsmo  10294  cfidm  10300  isfin3  10321  isfin5  10324  isfin6  10325  sdom2en01  10327  fin23lem26  10350  fin23lem30  10367  isf32lem5  10382  itunitc1  10445  ituniiun  10447  axdc3lem3  10477  axcclem  10482  axdclem  10544  iunfo  10564  iundom2g  10565  cardidg  10573  konigthlem  10593  alephadd  10602  alephreg  10607  pwcfsdom  10608  cfpwsdom  10609  elgch  10647  fpwwe2lem11  10666  canth4  10672  wunex2  10763  r1tskina  10807  elni  10901  nlt1pi  10931  adderpq  10981  mulerpq  10982  recmulnq  10989  addsrpr  11100  mulsrpr  11101  opelcn  11154  opelreal  11155  elreal  11156  elreal2  11157  0ncn  11158  addcnsr  11160  mulcnsr  11161  xrlenlt  11311  elnn0  12507  elnnne0  12519  un0addcl  12538  un0mulcl  12539  elxnn0  12579  uztrn2  12874  elnnuz  12899  elnn0uz  12900  elq  12967  elxr  13131  elfzm1b  13614  elfz0lmr  13783  uzrdgfni  13959  fzennn  13969  ser0  14055  hash2pwpr  14473  iswrd  14502  pfxccatpfx1  14722  s3iunsndisj  14951  sumz  15704  sumss  15706  fsumcvg3  15711  abscvgcvg  15801  isumshft  15821  prodf1  15873  zprod  15917  prod1  15924  prodss  15927  prodsn  15942  prodsnf  15944  bpolydiflem  16034  bpoly2  16037  bpoly3  16038  bpoly4  16039  ruclem6  16215  divides  16236  dvdsflip  16297  pwp1fsum  16371  sadc0  16432  eulerthlem2  16754  prm23lt5  16786  4sqlem2  16921  4sqlem12  16928  vdwpc  16952  xpscf  17550  cidpropd  17693  oppcsect  17764  funcpropd  17892  natpropd  17971  dfinito2  17995  dftermo2  17996  initoeu2lem0  18005  arwhoma  18037  eldmcoa  18057  pospo  18340  psss  18575  ismgmn0  18605  gsumpropd2lem  18642  elefmndbas  18833  smndex1basss  18865  smndex1mgm  18867  pwmnd  18897  dfgrp2e  18928  mulgfval  19033  eqg0subg  19159  cycsubmel  19163  ghmeqker  19206  elcntr  19293  cntri  19295  cntzsgrpcl  19297  oppgsubg  19329  fvcosymgeq  19396  symgfixels  19401  pmtrfrn  19425  efgsfo  19706  efgrelexlemb  19717  lt6abl  19862  dmdprd  19967  dprdval  19972  dprdw  19979  srgbinomlem4  20181  isnirred  20371  isrhm  20429  issrng  20742  lspexchn2  21031  lspindp2l  21034  lspindp2  21035  lbsextlem2  21059  rnglidl1  21140  df2idl2  21164  2idlss  21169  rngqiprngimfo  21208  cnfldfun  21310  cnfldfunOLD  21323  pzriprnglem3  21426  pzriprnglem4  21427  pzriprnglem7  21430  pzriprnglem8  21431  pzriprnglem9  21432  pzriprnglem12  21435  pzriprnglem14  21437  dsmmelbas  21690  frlmbas3  21727  lindsind2  21770  islindf4  21789  psrbagf  21868  evlslem4  22042  psdmul  22113  ply1bascl2  22147  cply1mul  22240  lply1binom  22254  matsubgcell  22380  matinvgcell  22381  matvscacell  22382  matepmcl  22408  matepm2cl  22409  scmatscm  22459  smatvscl  22470  marrepcl  22510  marepvcl  22515  mulmarep1el  22518  mulmarep1gsum1  22519  mulmarep1gsum2  22520  submabas  22524  m1detdiag  22543  mdetdiag  22545  m2detleib  22577  gsummatr01lem3  22603  gsummatr01  22605  smadiadetlem4  22615  slesolinv  22626  slesolinvbi  22627  slesolex  22628  cramerimplem2  22630  pmatcoe1fsupp  22647  mat2pmatbas  22672  mat2pmatmul  22677  mat2pmatlin  22681  decpmatmul  22718  monmatcollpw  22725  pm2mpf1  22745  pm2mpghm  22762  istps  22880  mretopd  23040  neiptopuni  23078  lpdifsn  23091  restcls  23129  perfopn  23133  pnfnei  23168  mnfnei  23169  lmss  23246  hauscmplem  23354  is2ndc  23394  2ndcdisj  23404  hausnlly  23441  txuni2  23513  ptpjpre1  23519  elpt  23520  dfac14  23566  xkococn  23608  fbasrn  23832  fin1aufil  23880  elfm2  23896  elfm3  23898  fbflim  23924  flffbas  23943  cnpflf2  23948  fclsbas  23969  efmndtmd  24049  tsmssubm  24091  iscusp2  24251  imasdsf1olem  24323  metustel  24503  metuel2  24518  isnghm  24684  opnreen  24791  iccpnfcnv  24913  ehleudisval  25391  ehl1eudis  25392  ehl2eudis  25394  minveclem3b  25400  ovoliunlem1  25475  ioombl1lem4  25534  subopnmbl  25577  vitalilem2  25582  vitalilem3  25583  mbfimaopnlem  25628  mbfimaopn2  25630  itg2l  25703  dvply1  26263  vieta1lem1  26290  vieta1lem2  26291  elaa  26296  taylthlem2  26354  taylthlem2OLD  26355  abelthlem6  26418  abelthlem9  26422  sinq34lt0t  26489  ellogrn  26538  dvrelog  26616  ellogdm  26618  logtayl2  26641  cxpcn3lem  26727  cxpcn3  26728  1cubr  26819  atandm  26853  atanf  26857  reasinsin  26873  atans2  26908  dmarea  26934  xrlimcnp  26945  amgmlem  26967  ppiublem1  27180  lgsdir2lem2  27304  gausslemma2dlem1a  27343  lgsquadlem1  27358  lgsquadlem2  27359  2sqlem1  27395  rpvmasum2  27490  madeval2  27826  newval  27828  leftval  27836  rightval  27837  lltropt  27845  madess  27849  oldssmade  27850  lrold  27869  addsproplem2  27933  addsproplem4  27935  addsproplem6  27937  negsproplem4  27989  negsproplem6  27991  precsexlem10  28164  precsexlem11  28165  sltonold  28203  elnns  28260  elzs  28283  edgiedgb  28939  isuhgr  28945  isushgr  28946  isupgr  28969  isumgr  28980  umgredg  29023  umgrpredgv  29025  umgredgne  29030  umgredgnlp  29032  isuspgr  29037  isusgr  29038  ausgrusgri  29053  usgredgppr  29081  edgssv2  29083  uspgredg2vlem  29108  uspgredg2v  29109  ushgredgedg  29114  ushgredgedgloop  29116  griedg0ssusgr  29150  uhgrissubgr  29160  subumgredg2  29170  uhgrspansubgrlem  29175  umgrres1lem  29195  upgrres1  29198  nbgrcl  29220  nbuhgr  29228  nbuhgr2vtx1edgblem  29236  nbupgrres  29249  edgnbusgreu  29252  nbusgredgeu0  29253  nbusgrf1o0  29254  hashnbusgrnn0  29261  nbupgruvtxres  29292  cffldtocusgr  29332  cffldtocusgrOLD  29333  cusgrfilem2  29342  vtxdg0v  29359  vtxduhgr0nedg  29378  uhgrvd00  29420  vtxdginducedm1  29429  finsumvtxdg2ssteplem4  29434  wlk1walk  29525  wlkp1lem6  29564  iswwlks  29719  wwlknllvtx  29729  wwlksonvtx  29738  wspthnonp  29742  wlkiswwlksupgr2  29760  wwlksnwwlksnon  29798  2pthon3v  29826  umgr2wlk  29832  elwwlks2s3  29834  wwlks2onv  29836  elwwlks2ons3im  29837  isclwwlk  29866  clwwlkccatlem  29871  clwlkclwwlk  29884  wwlksext2clwwlk  29939  hashecclwwlkn1  29959  umgrhashecclwwlk  29960  clwwlknon1  29979  clwwlknon1nloop  29981  clwwlknon2x  29985  1pthon2v  30035  uhgr3cyclex  30064  isconngr  30071  isconngr1  30072  eucrctshift  30125  frgrnbnb  30175  frgrncvvdeqlem1  30181  frgrncvvdeqlem2  30182  frgrncvvdeqlem3  30183  frgrncvvdeqlem9  30189  fusgreghash2wspv  30217  extwwlkfab  30234  numclwwlk1lem2foa  30236  numclwwlk1lem2fo  30240  clwlknon2num  30250  numclwlk2lem2f1o  30261  numclwwlk5lem  30269  topnfbey  30351  isvclem  30459  isnvlem  30492  vsfval  30515  h2hlm  30862  hhcmpl  31082  hhcms  31085  elch0  31136  omlsilem  31284  h1de2ctlem  31437  elspansni  31440  nonbooli  31533  spansncvi  31534  adjeq  31817  cnlnssadj  31962  cnvbraval  31992  brabgaf  32477  elimampt  32504  2ndresdju  32516  fmptdF  32523  fmptcof2  32524  acunirnmpt  32526  acunirnmpt2  32527  ofpreima  32532  fcnvgreu  32540  fdifsuppconst  32551  1stpreima  32568  2ndpreima  32569  fz2ssnn0  32635  elxrge02  32740  ccatws1f1o  32761  psgnfzto1stlem  32913  cycpmgcl  32966  nsgqusf1olem2  33226  nsgqusf1olem3  33227  prmidl0  33262  crngmxidl  33281  opprnsg  33296  rprmirredb  33344  zringfrac  33369  ply1degltel  33396  ply1degleel  33397  submatres  33538  lmat22lem  33549  crefdf  33580  cmppcmp  33590  rspectopn  33599  prsdm  33646  prsrn  33647  xrge0iifcnv  33665  xrge0iifiso  33667  xrge0iifhom  33669  pnfneige0  33683  qqhre  33752  rrhre  33753  esumnul  33798  esumcvgsum  33838  ldgenpisyslem1  33913  measvuni  33964  cntnevol  33978  dya2iocnrect  34032  sibf0  34085  oddpwdc  34105  eulerpartlemd  34117  eulerpartgbij  34123  eulerpartlemgh  34129  isrrvv  34194  coinfliprv  34233  ballotlem7  34286  signswch  34324  hashreprin  34383  chtvalz  34392  circlemethhgt  34406  hgt750lemb  34419  tgoldbachgt  34426  bnj23  34480  bnj158  34491  bnj168  34492  bnj1138  34550  bnj1143  34552  bnj1454  34604  bnj110  34620  bnj882  34688  bnj893  34690  bnj916  34695  bnj970  34709  bnj983  34713  bnj984  34714  bnj1137  34757  bnj1174  34765  bnj1388  34795  bnj1398  34796  loop1cycl  34878  subfacp1lem5  34925  satfv1  35104  satfrnmapom  35111  satf0op  35118  satf0n0  35119  fmlafvel  35126  fmlaomn0  35131  fmlan0  35132  satffunlem2lem2  35147  satfv0fvfmla0  35154  satefvfmla0  35159  mrsub0  35257  mrsubccat  35259  mrsubcn  35260  elmrsubrn  35261  msubco  35272  msubvrs  35301  elmthm  35317  mthmblem  35321  elrn3  35487  dfon2lem7  35516  brsset  35616  eltrans  35618  elfix  35630  ellimits  35637  elfuns  35642  elsingles  35645  fvtransport  35759  brcolinear2  35785  fvray  35868  linedegen  35870  fvline  35871  ellines  35879  fwddifn0  35891  elhf  35901  hfninf  35913  fnessref  35972  bj-ififc  36189  bj-csbsnlem  36512  bj-elgab  36548  currysetlem1  36557  bj-eltag  36587  bj-sngltag  36593  bj-projun  36604  bj-velpwALT  36663  bj-0nelmpt  36726  bj-opelidres  36771  bj-inftyexpitaudisj  36815  bj-elccinfty  36824  f1omptsnlem  36946  icoreelrnab  36964  relowlpssretop  36974  rdgssun  36988  exrecfnlem  36989  finxpnom  37011  uncov  37205  tan2h  37216  ptrecube  37224  poimirlem25  37249  poimirlem29  37253  poimirlem30  37254  poimirlem31  37255  poimirlem32  37256  cnambfre  37272  ftc1cnnc  37296  sdclem2  37346  sdclem1  37347  fdc  37349  caushft  37365  issmgrpOLD  37467  ismndo  37476  isrngo  37501  isdivrngo  37554  csbcom2fi  37732  elecALTV  37868  brrabga  37943  eldmcoss  38060  coss0  38081  elrels2  38088  dath  39339  diclspsn  40797  dvh4dimlem  41046  dvh2dim  41048  dvh3dim3N  41052  lcfrvalsnN  41144  mapdh6eN  41343  mapdh7dN  41353  mapdh8b  41383  hdmap1l6e  41417  lcmfunnnd  41615  3factsumint1  41624  primrootsunit1  41699  primrootscoprmpow  41702  aks6d1c2lem4  41730  sticksstones2  41750  sticksstones3  41751  sticksstones10  41758  sticksstones12a  41760  sticksstones12  41761  aks6d1c6lem2  41774  aks6d1c6lem3  41775  frlmfielbas  41878  mhpind  41962  elab2gw  42226  pellex  42397  rmspecnonsq  42469  islmodfg  42635  aaitgo  42728  areaquad  42786  ordeldif1o  42831  naddwordnexlem4  42973  fpwfvss  42984  finona1cl  43025  elcnvcnvintab  43154  elnonrel  43157  elcnvcnvlem  43171  cnvcnvintabd  43172  brfvrcld2  43264  grur1cld  43811  dvgrat  43891  cvgdvgrat  43892  radcnvrat  43893  nznngen  43895  uzmptshftfval  43925  binomcxplemcvg  43933  binomcxplemnotnn0  43935  tpid3gVD  44423  en3lplem2VD  44425  rexanuz3  44602  eliuniin  44605  eliuniin2  44626  disjinfi  44704  fsneq  44718  iuneqfzuzlem  44854  allbutfi  44913  eluzelz2  44923  uz0  44932  uzublem  44950  uzid3  44955  elicores  45056  uzinico  45083  climsuselem1  45133  climsuse  45134  islptre  45145  fnlimfvre  45200  limsupresico  45226  limsupvaluz  45234  limsupubuzlem  45238  limsupequzmptlem  45254  liminfresico  45297  cnrefiisplem  45355  stoweidlem14  45540  stoweidlem39  45565  stoweidlem48  45574  stoweidlem51  45577  stoweidlem59  45585  stoweidlem62  45588  wallispilem3  45593  fourierdlem42  45675  fourierdlem62  45694  fourierdlem80  45712  fourierdlem103  45735  fourierdlem104  45736  etransclem26  45786  rrxsnicc  45826  ioorrnopn  45831  ioorrnopnxr  45833  sge00  45902  sge0fodjrnlem  45942  sge0isum  45953  sge0seq  45972  meadjiunlem  45991  carageneld  46028  volicorescl  46079  hoidmv1lelem1  46117  hoidmv1le  46120  hoidmvlelem1  46121  hoidmvlelem3  46123  ovnhoilem2  46128  hoiqssbllem2  46149  opnvonmbllem2  46159  ovolval4lem1  46175  iinhoiicc  46200  vonioolem1  46206  smflimlem1  46297  smflimlem2  46298  smflim  46303  nsssmfmbf  46305  smfresal  46314  smfrec  46315  smfdiv  46323  smfpimbor1lem2  46325  smflim2  46332  smflimmpt  46336  smfinflem  46343  smfinfmpt  46345  smflimsuplem1  46346  smflimsuplem2  46347  smflimsuplem3  46348  smflimsuplem5  46350  smflimsuplem6  46351  smflimsup  46354  smflimsupmpt  46355  smfliminfmpt  46358  fcores  46587  ndmaovcl  46721  ndmaovcom  46723  ndmaovass  46724  ndmaovdistr  46725  dfatco  46774  otiunsndisjX  46797  fvmptrabdm  46811  elsetpreimafvb  46861  sprsymrelfolem2  46970  sprsymrelf  46972  sprsymrelf1  46973  prpair  46978  prproropf1olem0  46979  paireqne  46988  fmtno4prmfac  47049  dfodd5  47137  sbgoldbo  47264  nnsum4primeseven  47277  nnsum4primesevenALTV  47278  clnbgrcl  47298  sclnbgrel  47319  isuspgrim0  47356  isuspgrimlem  47358  gricushgr  47369  uspgrsprf  47394  uspgrsprf1  47395  uspgrsprfo  47396  opeliun2xp  47582  ply1sclrmsm  47637  lcoop  47665  lincfsuppcl  47667  linccl  47668  lincvalsng  47670  lincvalpr  47672  lincvalsc0  47675  linc0scn0  47677  lincdifsn  47678  linc1  47679  lincsum  47683  lincscm  47684  lspsslco  47691  snlindsntor  47725  lincresunit3lem2  47734  ldepsnlinclem1  47759  ldepsnlinclem2  47760  prelrrx2  47972  prelrrx2b  47973  rrx2xpref1o  47977  rrx2plord  47979  rrx2linesl  48002  oppcthin  48231  indthinc  48244  prsthinc  48246  elpglem3  48330