Theorem eleq2i 2826

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eleq12i  2827  eleqtri  2832  eleq2s  2852  hbxfreq  2865  nfceqi  2901  raleqbii  3339  rexeqbii  3340  rabeqi  3446  rabrabi  3451  reqabi  3455  elab2g  3670  elrabf  3679  elrab3t  3682  elrab2  3686  cbvsbcw  3811  cbvsbcvw  3812  cbvsbc  3813  elin2  4197  elsymdif  4247  noel  4330  noelOLD  4331  eltpg  4689  elunirab  4924  elintrab  4964  disjxiun  5145  exss  5463  otiunsndisj  5520  brabsb  5531  brabga  5534  epelg  5581  pofun  5606  elxp  5699  opeliunxp  5742  bropaex12  5766  brab2a  5768  elcnv  5875  dmopabelb  5915  elrnmptg  5957  elres  6019  elrid  6044  rninxp  6176  elid  6196  elsuci  6429  elsucg  6430  elsuc2g  6431  elfv  6887  0fv  6933  opabiota  6972  dffv2  6984  fvopab3g  6991  fvmptex  7010  fvopab5  7028  fvn0ssdmfun  7074  fveqressseq  7079  f0cli  7097  fmptco  7124  fvrnressn  7156  funfvima  7229  elunirnALT  7248  fliftel  7303  eloprabga  7513  eloprabgaOLD  7514  elrnmpo  7542  ovid  7546  offval  7676  sucexeloniOLD  7795  suceloniOLD  7797  1st2val  8000  2nd2val  8001  bropopvvv  8073  bropfvvvv  8075  fsplit  8100  xporderlem  8110  frpoins3xpg  8123  frpoins3xp3g  8124  brtpos2  8214  frrlem8  8275  frrlem9  8276  frrlem10  8277  fprresex  8292  wfrdmclOLD  8314  wfrfunOLD  8316  wfrlem12OLD  8317  wfrlem17OLD  8322  wfr2OLD  8325  issmo  8345  smores3  8350  tfrlem7  8380  tfrlem9  8382  tfrlem9a  8383  tfr2b  8393  tfr2  8395  rdgsuc  8421  frsucmptn  8436  tz7.48-2  8439  el1o  8492  ord2eln012  8494  dif1o  8497  ondif2  8499  oawordeulem  8551  elecg  8743  brecop  8801  erovlem  8804  eceqoveq  8813  mapsncnv  8884  mptelixpg  8926  brsdom  8968  isfi  8969  enssdom  8970  brdom2  8975  xpcomco  9059  brsdom2  9094  en3lplem2  9605  cnfcom2lem  9693  brttrcl2  9706  ttrcltr  9708  rnttrcl  9714  epfrs  9723  r1limg  9763  r1ord  9772  r1ord3  9774  tz9.12lem3  9781  rankvaln  9791  r1elss  9798  rankpwi  9815  ssrankr1  9827  r1val3  9830  r1pw  9837  rankr1b  9856  djur  9911  djuunxp  9913  eldju2ndl  9916  eldju2ndr  9917  isnum2  9937  cardprclem  9971  infxpenlem  10005  alephcard  10062  alephnbtwn  10063  alephnbtwn2  10064  alephord2  10068  alephsdom  10078  dfac3  10113  dfac5lem2  10116  dfac5lem3  10117  dfac5lem5  10119  pwsdompw  10196  cfub  10241  cardcf  10244  cflecard  10245  cfle  10246  cflim2  10255  cofsmo  10261  cfidm  10267  isfin3  10288  isfin5  10291  isfin6  10292  sdom2en01  10294  fin23lem26  10317  fin23lem30  10334  isf32lem5  10349  itunitc1  10412  ituniiun  10414  axdc3lem3  10444  axcclem  10449  axdclem  10511  iunfo  10531  iundom2g  10532  cardidg  10540  konigthlem  10560  alephadd  10569  alephreg  10574  pwcfsdom  10575  cfpwsdom  10576  elgch  10614  fpwwe2lem11  10633  canth4  10639  wunex2  10730  r1tskina  10774  elni  10868  nlt1pi  10898  adderpq  10948  mulerpq  10949  recmulnq  10956  addsrpr  11067  mulsrpr  11068  opelcn  11121  opelreal  11122  elreal  11123  elreal2  11124  0ncn  11125  addcnsr  11127  mulcnsr  11128  xrlenlt  11276  elnn0  12471  elnnne0  12483  un0addcl  12502  un0mulcl  12503  elxnn0  12543  uztrn2  12838  elnnuz  12863  elnn0uz  12864  elq  12931  elxr  13093  elfzm1b  13576  elfz0lmr  13744  uzrdgfni  13920  fzennn  13930  ser0  14017  hash2pwpr  14434  iswrd  14463  pfxccatpfx1  14683  s3iunsndisj  14912  sumz  15665  sumss  15667  fsumcvg3  15672  abscvgcvg  15762  isumshft  15782  prodf1  15834  zprod  15878  prod1  15885  prodss  15888  prodsn  15903  prodsnf  15905  bpolydiflem  15995  bpoly2  15998  bpoly3  15999  bpoly4  16000  ruclem6  16175  divides  16196  dvdsflip  16257  pwp1fsum  16331  sadc0  16392  eulerthlem2  16712  prm23lt5  16744  4sqlem2  16879  4sqlem12  16886  vdwpc  16910  xpscf  17508  cidpropd  17651  oppcsect  17722  funcpropd  17848  natpropd  17926  dfinito2  17950  dftermo2  17951  initoeu2lem0  17960  arwhoma  17992  eldmcoa  18012  pospo  18295  psss  18530  ismgmn0  18560  gsumpropd2lem  18595  elefmndbas  18751  smndex1basss  18783  smndex1mgm  18785  pwmnd  18815  dfgrp2e  18845  mulgfval  18947  eqg0subg  19068  cycsubmel  19072  ghmeqker  19114  elcntr  19189  cntri  19191  cntzsgrpcl  19193  oppgsubg  19225  fvcosymgeq  19292  symgfixels  19297  pmtrfrn  19321  efgsfo  19602  efgrelexlemb  19613  lt6abl  19758  dmdprd  19863  dprdval  19868  dprdw  19875  srgbinomlem4  20046  isnirred  20227  isrhm  20250  issrng  20451  lspexchn2  20737  lspindp2l  20740  lspindp2  20741  lbsextlem2  20765  2idlss  20861  cnfldfun  20949  dsmmelbas  21286  frlmbas3  21323  lindsind2  21366  islindf4  21385  psrbagf  21463  evlslem4  21629  ply1bascl2  21720  cply1mul  21810  lply1binom  21822  matsubgcell  21928  matinvgcell  21929  matvscacell  21930  matepmcl  21956  matepm2cl  21957  scmatscm  22007  smatvscl  22018  marrepcl  22058  marepvcl  22063  mulmarep1el  22066  mulmarep1gsum1  22067  mulmarep1gsum2  22068  submabas  22072  m1detdiag  22091  mdetdiag  22093  m2detleib  22125  gsummatr01lem3  22151  gsummatr01  22153  smadiadetlem4  22163  slesolinv  22174  slesolinvbi  22175  slesolex  22176  cramerimplem2  22178  pmatcoe1fsupp  22195  mat2pmatbas  22220  mat2pmatmul  22225  mat2pmatlin  22229  decpmatmul  22266  monmatcollpw  22273  pm2mpf1  22293  pm2mpghm  22310  istps  22428  mretopd  22588  neiptopuni  22626  lpdifsn  22639  restcls  22677  perfopn  22681  pnfnei  22716  mnfnei  22717  lmss  22794  hauscmplem  22902  is2ndc  22942  2ndcdisj  22952  hausnlly  22989  txuni2  23061  ptpjpre1  23067  elpt  23068  dfac14  23114  xkococn  23156  fbasrn  23380  fin1aufil  23428  elfm2  23444  elfm3  23446  fbflim  23472  flffbas  23491  cnpflf2  23496  fclsbas  23517  efmndtmd  23597  tsmssubm  23639  iscusp2  23799  imasdsf1olem  23871  metustel  24051  metuel2  24066  isnghm  24232  opnreen  24339  iccpnfcnv  24452  ehleudisval  24928  ehl1eudis  24929  ehl2eudis  24931  minveclem3b  24937  ovoliunlem1  25011  ioombl1lem4  25070  subopnmbl  25113  vitalilem2  25118  vitalilem3  25119  mbfimaopnlem  25164  mbfimaopn2  25166  itg2l  25239  dvply1  25789  vieta1lem1  25815  vieta1lem2  25816  elaa  25821  taylthlem2  25878  abelthlem6  25940  abelthlem9  25944  sinq34lt0t  26011  ellogrn  26060  dvrelog  26137  ellogdm  26139  logtayl2  26162  cxpcn3lem  26245  cxpcn3  26246  1cubr  26337  atandm  26371  atanf  26375  reasinsin  26391  atans2  26426  dmarea  26452  xrlimcnp  26463  amgmlem  26484  ppiublem1  26695  lgsdir2lem2  26819  gausslemma2dlem1a  26858  lgsquadlem1  26873  lgsquadlem2  26874  2sqlem1  26910  rpvmasum2  27005  madeval2  27338  newval  27340  leftval  27348  rightval  27349  lltropt  27357  madess  27361  oldssmade  27362  lrold  27381  addsproplem2  27444  addsproplem4  27446  addsproplem6  27448  negsproplem4  27495  negsproplem6  27497  precsexlem10  27652  precsexlem11  27653  edgiedgb  28304  isuhgr  28310  isushgr  28311  isupgr  28334  isumgr  28345  umgredg  28388  umgrpredgv  28390  umgredgne  28395  umgredgnlp  28397  isuspgr  28402  isusgr  28403  ausgrusgri  28418  usgredgppr  28443  edgssv2  28445  uspgredg2vlem  28470  uspgredg2v  28471  ushgredgedg  28476  ushgredgedgloop  28478  griedg0ssusgr  28512  uhgrissubgr  28522  subumgredg2  28532  uhgrspansubgrlem  28537  umgrres1lem  28557  upgrres1  28560  nbgrcl  28582  nbuhgr  28590  nbuhgr2vtx1edgblem  28598  nbupgrres  28611  edgnbusgreu  28614  nbusgredgeu0  28615  nbusgrf1o0  28616  hashnbusgrnn0  28623  nbupgruvtxres  28654  cffldtocusgr  28694  cusgrfilem2  28703  vtxdg0v  28720  vtxduhgr0nedg  28739  uhgrvd00  28781  vtxdginducedm1  28790  finsumvtxdg2ssteplem4  28795  wlk1walk  28886  wlkp1lem6  28925  iswwlks  29080  wwlknllvtx  29090  wwlksonvtx  29099  wspthnonp  29103  wlkiswwlksupgr2  29121  wwlksnwwlksnon  29159  2pthon3v  29187  umgr2wlk  29193  elwwlks2s3  29195  wwlks2onv  29197  elwwlks2ons3im  29198  isclwwlk  29227  clwwlkccatlem  29232  clwlkclwwlk  29245  wwlksext2clwwlk  29300  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  clwwlknon1  29340  clwwlknon1nloop  29342  clwwlknon2x  29346  1pthon2v  29396  uhgr3cyclex  29425  isconngr  29432  isconngr1  29433  eucrctshift  29486  frgrnbnb  29536  frgrncvvdeqlem1  29542  frgrncvvdeqlem2  29543  frgrncvvdeqlem3  29544  frgrncvvdeqlem9  29550  fusgreghash2wspv  29578  extwwlkfab  29595  numclwwlk1lem2foa  29597  numclwwlk1lem2fo  29601  clwlknon2num  29611  numclwlk2lem2f1o  29622  numclwwlk5lem  29630  topnfbey  29712  isvclem  29818  isnvlem  29851  vsfval  29874  h2hlm  30221  hhcmpl  30441  hhcms  30444  elch0  30495  omlsilem  30643  h1de2ctlem  30796  elspansni  30799  nonbooli  30892  spansncvi  30893  adjeq  31176  cnlnssadj  31321  cnvbraval  31351  brabgaf  31825  elimampt  31850  2ndresdju  31862  fmptdF  31869  fmptcof2  31870  acunirnmpt  31872  acunirnmpt2  31873  ofpreima  31878  fcnvgreu  31886  fdifsuppconst  31899  1stpreima  31916  2ndpreima  31917  fz2ssnn0  31984  elxrge02  32086  psgnfzto1stlem  32247  cycpmgcl  32300  nsgqusf1olem2  32514  nsgqusf1olem3  32515  prmidl0  32558  crngmxidl  32574  opprnsg  32587  ply1degltel  32655  submatres  32775  lmat22lem  32786  crefdf  32817  cmppcmp  32827  rspectopn  32836  prsdm  32883  prsrn  32884  xrge0iifcnv  32902  xrge0iifiso  32904  xrge0iifhom  32906  pnfneige0  32920  qqhre  32989  rrhre  32990  esumnul  33035  esumcvgsum  33075  ldgenpisyslem1  33150  measvuni  33201  cntnevol  33215  dya2iocnrect  33269  sibf0  33322  oddpwdc  33342  eulerpartlemd  33354  eulerpartgbij  33360  eulerpartlemgh  33366  isrrvv  33431  coinfliprv  33470  ballotlem7  33523  signswch  33561  hashreprin  33621  chtvalz  33630  circlemethhgt  33644  hgt750lemb  33657  tgoldbachgt  33664  bnj23  33718  bnj158  33729  bnj168  33730  bnj1138  33788  bnj1143  33790  bnj1454  33842  bnj110  33858  bnj882  33926  bnj893  33928  bnj916  33933  bnj970  33947  bnj983  33951  bnj984  33952  bnj1137  33995  bnj1174  34003  bnj1388  34033  bnj1398  34034  loop1cycl  34117  subfacp1lem5  34164  satfv1  34343  satfrnmapom  34350  satf0op  34357  satf0n0  34358  fmlafvel  34365  fmlaomn0  34370  fmlan0  34371  satffunlem2lem2  34386  satfv0fvfmla0  34393  satefvfmla0  34398  mrsub0  34496  mrsubccat  34498  mrsubcn  34499  elmrsubrn  34500  msubco  34511  msubvrs  34540  elmthm  34556  mthmblem  34560  elrn3  34721  dfon2lem7  34750  brsset  34850  eltrans  34852  elfix  34864  ellimits  34871  elfuns  34876  elsingles  34879  fvtransport  34993  brcolinear2  35019  fvray  35102  linedegen  35104  fvline  35105  ellines  35113  fwddifn0  35125  elhf  35135  hfninf  35147  fnessref  35231  bj-ififc  35448  bj-csbsnlem  35772  bj-elgab  35808  currysetlem1  35817  bj-eltag  35847  bj-sngltag  35853  bj-projun  35864  bj-velpwALT  35923  bj-0nelmpt  35986  bj-opelidres  36031  bj-inftyexpitaudisj  36075  bj-elccinfty  36084  f1omptsnlem  36206  icoreelrnab  36224  relowlpssretop  36234  rdgssun  36248  exrecfnlem  36249  finxpnom  36271  uncov  36458  tan2h  36469  ptrecube  36477  poimirlem25  36502  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimirlem32  36509  cnambfre  36525  ftc1cnnc  36549  sdclem2  36599  sdclem1  36600  fdc  36602  caushft  36618  issmgrpOLD  36720  ismndo  36729  isrngo  36754  isdivrngo  36807  csbcom2fi  36985  elecALTV  37123  brrabga  37199  eldmcoss  37317  coss0  37338  elrels2  37345  dath  38596  diclspsn  40054  dvh4dimlem  40303  dvh2dim  40305  dvh3dim3N  40309  lcfrvalsnN  40401  mapdh6eN  40600  mapdh7dN  40610  mapdh8b  40640  hdmap1l6e  40674  lcmfunnnd  40866  3factsumint1  40875  sticksstones2  40952  sticksstones3  40953  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  elab2gw  41015  frlmfielbas  41072  mhpind  41164  pellex  41559  rmspecnonsq  41631  islmodfg  41797  aaitgo  41890  areaquad  41951  ordeldif1o  41996  naddwordnexlem4  42138  fpwfvss  42149  finona1cl  42190  elcnvcnvintab  42319  elnonrel  42322  elcnvcnvlem  42336  cnvcnvintabd  42337  brfvrcld2  42429  grur1cld  42977  dvgrat  43057  cvgdvgrat  43058  radcnvrat  43059  nznngen  43061  uzmptshftfval  43091  binomcxplemcvg  43099  binomcxplemnotnn0  43101  tpid3gVD  43589  en3lplem2VD  43591  rexanuz3  43771  eliuniin  43774  eliuniin2  43795  disjinfi  43877  fsneq  43891  iuneqfzuzlem  44031  allbutfi  44090  eluzelz2  44100  uz0  44109  uzublem  44127  uzid3  44132  elicores  44233  uzinico  44260  climsuselem1  44310  climsuse  44311  islptre  44322  fnlimfvre  44377  limsupresico  44403  limsupvaluz  44411  limsupubuzlem  44415  limsupequzmptlem  44431  liminfresico  44474  cnrefiisplem  44532  stoweidlem14  44717  stoweidlem39  44742  stoweidlem48  44751  stoweidlem51  44754  stoweidlem59  44762  stoweidlem62  44765  wallispilem3  44770  fourierdlem42  44852  fourierdlem62  44871  fourierdlem80  44889  fourierdlem103  44912  fourierdlem104  44913  etransclem26  44963  rrxsnicc  45003  ioorrnopn  45008  ioorrnopnxr  45010  sge00  45079  sge0fodjrnlem  45119  sge0isum  45130  sge0seq  45149  meadjiunlem  45168  carageneld  45205  volicorescl  45256  hoidmv1lelem1  45294  hoidmv1le  45297  hoidmvlelem1  45298  hoidmvlelem3  45300  ovnhoilem2  45305  hoiqssbllem2  45326  opnvonmbllem2  45336  ovolval4lem1  45352  iinhoiicc  45377  vonioolem1  45383  smflimlem1  45474  smflimlem2  45475  smflim  45480  nsssmfmbf  45482  smfresal  45491  smfrec  45492  smfdiv  45500  smfpimbor1lem2  45502  smflim2  45509  smflimmpt  45513  smfinflem  45520  smfinfmpt  45522  smflimsuplem1  45523  smflimsuplem2  45524  smflimsuplem3  45525  smflimsuplem5  45527  smflimsuplem6  45528  smflimsup  45531  smflimsupmpt  45532  smfliminfmpt  45535  fcores  45764  ndmaovcl  45898  ndmaovcom  45900  ndmaovass  45901  ndmaovdistr  45902  dfatco  45951  otiunsndisjX  45974  fvmptrabdm  45988  elsetpreimafvb  46039  sprsymrelfolem2  46148  sprsymrelf  46150  sprsymrelf1  46151  prpair  46156  prproropf1olem0  46157  paireqne  46166  fmtno4prmfac  46227  dfodd5  46315  sbgoldbo  46442  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  isomushgr  46481  isomuspgrlem2c  46485  uspgrsprf  46511  uspgrsprf1  46512  uspgrsprfo  46513  rnglidl1  46736  rngqiprngimfo  46767  opeliun2xp  46962  ply1sclrmsm  47018  lcoop  47046  lincfsuppcl  47048  linccl  47049  lincvalsng  47051  lincvalpr  47053  lincvalsc0  47056  linc0scn0  47058  lincdifsn  47059  linc1  47060  lincsum  47064  lincscm  47065  lspsslco  47072  snlindsntor  47106  lincresunit3lem2  47115  ldepsnlinclem1  47140  ldepsnlinclem2  47141  prelrrx2  47353  prelrrx2b  47354  rrx2xpref1o  47358  rrx2plord  47360  rrx2linesl  47383  oppcthin  47613  indthinc  47626  prsthinc  47628  elpglem3  47712