Theorem eleq2i 2906

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  eleq12i  2907  eleqtri  2913  eleq2s  2933  hbxfreq  2944  nfceqi  2975  raleqbii  3236  rexeqbii  3328  rabeq2i  3489  elab2g  3670  elrabf  3678  elrab3t  3681  elrab2  3685  cbvsbcw  3806  cbvsbc  3808  elin2  4176  elsymdif  4226  dfnul2OLD  4296  noel  4298  noelOLD  4299  eltpg  4625  elunirab  4856  elintrab  4890  disjxiun  5065  exss  5357  otiunsndisj  5412  brabsb  5420  brabga  5423  epelg  5468  pofun  5493  elxp  5580  opeliunxp  5621  bropaex12  5644  brab2a  5646  elcnv  5749  dmopabelb  5787  elrnmptg  5833  elres  5893  elrid  5915  rninxp  6038  elid  6058  elsuci  6259  elsucg  6260  elsuc2g  6261  elfv  6670  0fv  6711  opabiota  6748  dffv2  6758  fvopab3g  6765  fvmptex  6784  fvopab5  6802  fvn0ssdmfun  6844  fveqressseq  6849  f0cli  6866  fmptco  6893  fvrnressn  6925  funfvima  6994  elunirnALT  7013  fliftel  7064  eloprabga  7263  elrnmpo  7289  ovid  7293  offval  7418  suceloni  7530  1st2val  7719  2nd2val  7720  bropopvvv  7787  bropfvvvv  7789  fsplit  7814  fsplitOLD  7815  xporderlem  7823  brtpos2  7900  wfrdmcl  7965  wfrfun  7967  wfrlem12  7968  wfrlem17  7973  wfr2  7976  issmo  7987  smores3  7992  tfrlem7  8021  tfrlem9  8023  tfrlem9a  8024  tfr2b  8034  tfr2  8036  rdgsuc  8062  frsucmptn  8076  tz7.48-2  8080  el1o  8126  dif1o  8127  ondif2  8129  oawordeulem  8182  elecg  8334  brecop  8392  erovlem  8395  eceqoveq  8404  mapsncnv  8459  mptelixpg  8501  brsdom  8534  isfi  8535  enssdom  8536  brdom2  8541  xpcomco  8609  brsdom2  8643  en3lplem2  9078  cnfcom2lem  9166  epfrs  9175  r1limg  9202  r1ord  9211  r1ord3  9213  tz9.12lem3  9220  rankvaln  9230  r1elss  9237  rankpwi  9254  ssrankr1  9266  r1val3  9269  r1pw  9276  rankr1b  9295  djur  9350  djuunxp  9352  eldju2ndl  9355  eldju2ndr  9356  isnum2  9376  cardprclem  9410  infxpenlem  9441  alephcard  9498  alephnbtwn  9499  alephnbtwn2  9500  alephord2  9504  alephsdom  9514  dfac3  9549  dfac5lem2  9552  dfac5lem3  9553  dfac5lem5  9555  pwsdompw  9628  cfub  9673  cardcf  9676  cflecard  9677  cfle  9678  cflim2  9687  cofsmo  9693  cfidm  9699  isfin3  9720  isfin5  9723  isfin6  9724  sdom2en01  9726  fin23lem26  9749  fin23lem30  9766  isf32lem5  9781  itunitc1  9844  ituniiun  9846  axdc3lem3  9876  axcclem  9881  axdclem  9943  iunfo  9963  iundom2g  9964  cardidg  9972  konigthlem  9992  alephadd  10001  alephreg  10006  pwcfsdom  10007  cfpwsdom  10008  elgch  10046  fpwwe2lem12  10065  canth4  10071  wunex2  10162  r1tskina  10206  elni  10300  nlt1pi  10330  adderpq  10380  mulerpq  10381  recmulnq  10388  addsrpr  10499  mulsrpr  10500  opelcn  10553  opelreal  10554  elreal  10555  elreal2  10556  0ncn  10557  addcnsr  10559  mulcnsr  10560  xrlenlt  10708  elnn0  11902  elnnne0  11914  un0addcl  11933  un0mulcl  11934  elxnn0  11972  uztrn2  12265  elnnuz  12285  elnn0uz  12286  elq  12353  elxr  12514  elfzm1b  12988  elfz0lmr  13155  uzrdgfni  13329  fzennn  13339  ser0  13425  hash2pwpr  13837  iswrd  13866  pfxccatpfx1  14100  s3iunsndisj  14330  sumz  15081  sumss  15083  fsumcvg3  15088  abscvgcvg  15176  isumshft  15196  prodf1  15249  zprod  15293  prod1  15300  prodss  15303  prodsn  15318  prodsnf  15320  bpolydiflem  15410  bpoly2  15413  bpoly3  15414  bpoly4  15415  ruclem6  15590  divides  15611  dvdsflip  15669  pwp1fsum  15744  sadc0  15805  eulerthlem2  16121  prm23lt5  16153  4sqlem2  16287  4sqlem12  16294  vdwpc  16318  xpscf  16840  cidpropd  16982  oppcsect  17050  funcpropd  17172  natpropd  17248  initoeu2lem0  17275  arwhoma  17307  eldmcoa  17327  pospo  17585  psss  17826  ismgmn0  17856  gsumpropd2lem  17891  elefmndbas  18040  smndex1basss  18072  smndex1mgm  18074  pwmnd  18104  dfgrp2e  18131  mulgfval  18228  cycsubmel  18345  ghmeqker  18387  cntri  18463  oppgsubg  18493  fvcosymgeq  18559  symgfixels  18564  pmtrfrn  18588  efgsfo  18867  efgrelexlemb  18878  lt6abl  19017  dmdprd  19122  dprdval  19127  dprdw  19134  srgbinomlem4  19295  isnirred  19452  isrhm  19475  issrng  19623  lspexchn2  19905  lspindp2l  19908  lspindp2  19909  lbsextlem2  19933  evlslem4  20290  ply1bascl2  20374  cply1mul  20464  lply1binom  20476  cnfldfunALT  20560  dsmmelbas  20885  frlmbas3  20922  lindsind2  20965  islindf4  20984  matsubgcell  21045  matinvgcell  21046  matvscacell  21047  matepmcl  21073  matepm2cl  21074  scmatscm  21124  smatvscl  21135  marrepcl  21175  marepvcl  21180  mulmarep1el  21183  mulmarep1gsum1  21184  mulmarep1gsum2  21185  submabas  21189  m1detdiag  21208  mdetdiag  21210  m2detleib  21242  gsummatr01lem3  21268  gsummatr01  21270  smadiadetlem4  21280  slesolinv  21291  slesolinvbi  21292  slesolex  21293  cramerimplem2  21295  pmatcoe1fsupp  21311  mat2pmatbas  21336  mat2pmatmul  21341  mat2pmatlin  21345  decpmatmul  21382  monmatcollpw  21389  pm2mpf1  21409  pm2mpghm  21426  istps  21544  mretopd  21702  neiptopuni  21740  lpdifsn  21753  restcls  21791  perfopn  21795  pnfnei  21830  mnfnei  21831  lmss  21908  hauscmplem  22016  is2ndc  22056  2ndcdisj  22066  hausnlly  22103  txuni2  22175  ptpjpre1  22181  elpt  22182  dfac14  22228  xkococn  22270  fbasrn  22494  fin1aufil  22542  elfm2  22558  elfm3  22560  fbflim  22586  flffbas  22605  cnpflf2  22610  fclsbas  22631  efmndtmd  22711  tsmssubm  22753  iscusp2  22913  imasdsf1olem  22985  metustel  23162  metuel2  23177  isnghm  23334  opnreen  23441  iccpnfcnv  23550  ehleudisval  24024  ehl1eudis  24025  ehl2eudis  24027  minveclem3b  24033  ovoliunlem1  24105  ioombl1lem4  24164  subopnmbl  24207  vitalilem2  24212  vitalilem3  24213  mbfimaopnlem  24258  mbfimaopn2  24260  itg2l  24332  dvply1  24875  vieta1lem1  24901  vieta1lem2  24902  elaa  24907  taylthlem2  24964  abelthlem6  25026  abelthlem9  25030  sinq34lt0t  25097  ellogrn  25145  dvrelog  25222  ellogdm  25224  logtayl2  25247  cxpcn3lem  25330  cxpcn3  25331  1cubr  25422  atandm  25456  atanf  25460  reasinsin  25476  atans2  25511  dmarea  25537  xrlimcnp  25548  amgmlem  25569  ppiublem1  25780  lgsdir2lem2  25904  gausslemma2dlem1a  25943  lgsquadlem1  25958  lgsquadlem2  25959  2sqlem1  25995  rpvmasum2  26090  edgiedgb  26841  isuhgr  26847  isushgr  26848  isupgr  26871  isumgr  26882  umgredg  26925  umgrpredgv  26927  umgredgne  26932  umgredgnlp  26934  isuspgr  26939  isusgr  26940  ausgrusgri  26955  usgredgppr  26980  edgssv2  26982  uspgredg2vlem  27007  uspgredg2v  27008  ushgredgedg  27013  ushgredgedgloop  27015  griedg0ssusgr  27049  uhgrissubgr  27059  subumgredg2  27069  uhgrspansubgrlem  27074  umgrres1lem  27094  upgrres1  27097  nbgrcl  27119  nbuhgr  27127  nbuhgr2vtx1edgblem  27135  nbupgrres  27148  edgnbusgreu  27151  nbusgredgeu0  27152  nbusgrf1o0  27153  hashnbusgrnn0  27160  nbupgruvtxres  27191  cffldtocusgr  27231  cusgrfilem2  27240  vtxdg0v  27257  vtxduhgr0nedg  27276  uhgrvd00  27318  vtxdginducedm1  27327  finsumvtxdg2ssteplem4  27332  wlk1walk  27422  wlkp1lem6  27462  iswwlks  27616  wwlknllvtx  27626  wwlksonvtx  27635  wspthnonp  27639  wlkiswwlksupgr2  27657  wwlksnwwlksnon  27696  2pthon3v  27724  umgr2wlk  27730  elwwlks2s3  27732  wwlks2onv  27734  elwwlks2ons3im  27735  isclwwlk  27764  clwwlkccatlem  27769  clwlkclwwlk  27782  wwlksext2clwwlk  27838  hashecclwwlkn1  27858  umgrhashecclwwlk  27859  clwwlknon1  27878  clwwlknon1nloop  27880  clwwlknon2x  27884  1pthon2v  27934  uhgr3cyclex  27963  isconngr  27970  isconngr1  27971  eucrctshift  28024  frgrnbnb  28074  frgrncvvdeqlem1  28080  frgrncvvdeqlem2  28081  frgrncvvdeqlem3  28082  frgrncvvdeqlem9  28088  fusgreghash2wspv  28116  extwwlkfab  28133  numclwwlk1lem2foa  28135  numclwwlk1lem2fo  28139  clwlknon2num  28149  numclwlk2lem2f1o  28160  numclwwlk5lem  28168  topnfbey  28250  isvclem  28356  isnvlem  28389  vsfval  28412  h2hlm  28759  hhcmpl  28979  hhcms  28982  elch0  29033  omlsilem  29181  h1de2ctlem  29334  elspansni  29337  nonbooli  29430  spansncvi  29431  adjeq  29714  cnlnssadj  29859  cnvbraval  29889  brabgaf  30361  elimampt  30385  fmptdF  30403  fmptcof2  30404  acunirnmpt  30406  acunirnmpt2  30407  ofpreima  30412  fcnvgreu  30420  1stpreima  30444  2ndpreima  30445  fz2ssnn0  30510  elxrge02  30610  psgnfzto1stlem  30744  cycpmgcl  30797  submatres  31073  lmat22lem  31084  crefdf  31114  cmppcmp  31124  prsdm  31159  prsrn  31160  xrge0iifcnv  31178  xrge0iifiso  31180  xrge0iifhom  31182  pnfneige0  31196  qqhre  31263  rrhre  31264  esumnul  31309  esumcvgsum  31349  ldgenpisyslem1  31424  measvuni  31475  cntnevol  31489  dya2iocnrect  31541  sibf0  31594  oddpwdc  31614  eulerpartlemd  31626  eulerpartgbij  31632  eulerpartlemgh  31638  isrrvv  31703  coinfliprv  31742  ballotlem7  31795  signswch  31833  hashreprin  31893  chtvalz  31902  circlemethhgt  31916  hgt750lemb  31929  tgoldbachgt  31936  bnj23  31990  bnj158  32001  bnj168  32002  bnj1138  32062  bnj1143  32064  bnj1454  32116  bnj110  32132  bnj882  32200  bnj893  32202  bnj916  32207  bnj970  32221  bnj983  32225  bnj984  32226  bnj1137  32269  bnj1174  32277  bnj1388  32307  bnj1398  32308  loop1cycl  32386  subfacp1lem5  32433  satfv1  32612  satfrnmapom  32619  satf0op  32626  satf0n0  32627  fmlafvel  32634  fmlaomn0  32639  fmlan0  32640  satffunlem2lem2  32655  satfv0fvfmla0  32662  satefvfmla0  32667  mrsub0  32765  mrsubccat  32767  mrsubcn  32768  elmrsubrn  32769  msubco  32780  msubvrs  32809  elmthm  32825  mthmblem  32829  elrn3  33000  dfon2lem7  33036  eltrpred  33067  frrlem8  33132  frrlem9  33133  frrlem10  33134  madeval2  33292  brsset  33352  eltrans  33354  elfix  33366  ellimits  33373  elfuns  33378  elsingles  33381  fvtransport  33495  brcolinear2  33521  fvray  33604  linedegen  33606  fvline  33607  ellines  33615  fwddifn0  33627  elhf  33637  hfninf  33649  fnessref  33707  bj-ififc  33917  bj-csbsnlem  34222  currysetlem1  34260  bj-eltag  34291  bj-sngltag  34297  bj-projun  34308  bj-0nelmpt  34410  bj-opelidres  34455  bj-inftyexpitaudisj  34489  bj-elccinfty  34498  f1omptsnlem  34619  icoreelrnab  34637  relowlpssretop  34647  rdgssun  34661  exrecfnlem  34662  finxpnom  34684  uncov  34875  tan2h  34886  ptrecube  34894  poimirlem25  34919  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  poimirlem32  34926  cnambfre  34942  ftc1cnnc  34968  sdclem2  35019  sdclem1  35020  fdc  35022  caushft  35038  issmgrpOLD  35143  ismndo  35152  isrngo  35177  isdivrngo  35230  csbcom2fi  35408  elecALTV  35529  brrabga  35600  eldmcoss  35700  coss0  35721  elrels2  35728  dath  36874  diclspsn  38332  dvh4dimlem  38581  dvh2dim  38583  dvh3dim3N  38587  lcfrvalsnN  38679  mapdh6eN  38878  mapdh7dN  38888  mapdh8b  38918  hdmap1l6e  38952  frlmfielbas  39146  pellex  39439  rmspecnonsq  39511  islmodfg  39676  aaitgo  39769  areaquad  39830  elcnvcnvintab  39949  elnonrel  39952  elcnvcnvlem  39966  cnvcnvintabd  39967  brfvrcld2  40044  grur1cld  40575  dvgrat  40651  cvgdvgrat  40652  radcnvrat  40653  nznngen  40655  uzmptshftfval  40685  binomcxplemcvg  40693  binomcxplemnotnn0  40695  tpid3gVD  41183  en3lplem2VD  41185  rexanuz3  41369  eliuniin  41372  eliuniin2  41393  disjinfi  41461  fsneq  41476  iuneqfzuzlem  41609  allbutfi  41672  eluzelz2  41683  uz0  41693  uzublem  41711  uzid3  41716  elicores  41816  uzinico  41843  climsuselem1  41895  climsuse  41896  islptre  41907  fnlimfvre  41962  limsupresico  41988  limsupvaluz  41996  limsupubuzlem  42000  limsupequzmptlem  42016  liminfresico  42059  cnrefiisplem  42117  stoweidlem14  42306  stoweidlem39  42331  stoweidlem48  42340  stoweidlem51  42343  stoweidlem59  42351  stoweidlem62  42354  wallispilem3  42359  fourierdlem42  42441  fourierdlem62  42460  fourierdlem80  42478  fourierdlem103  42501  fourierdlem104  42502  etransclem26  42552  rrxsnicc  42592  ioorrnopn  42597  ioorrnopnxr  42599  sge00  42665  sge0fodjrnlem  42705  sge0isum  42716  sge0seq  42735  meadjiunlem  42754  carageneld  42791  volicorescl  42842  hoidmv1lelem1  42880  hoidmv1le  42883  hoidmvlelem1  42884  hoidmvlelem3  42886  ovnhoilem2  42891  hoiqssbllem2  42912  opnvonmbllem2  42922  ovolval4lem1  42938  iinhoiicc  42963  vonioolem1  42969  smflimlem1  43054  smflimlem2  43055  smflim  43060  nsssmfmbf  43062  smfresal  43070  smfrec  43071  smfdiv  43079  smfpimbor1lem2  43081  smflim2  43087  smflimmpt  43091  smfsupmpt  43096  smfinflem  43098  smfinfmpt  43100  smflimsuplem1  43101  smflimsuplem2  43102  smflimsuplem3  43103  smflimsuplem5  43105  smflimsuplem6  43106  smflimsup  43109  smflimsupmpt  43110  smfliminfmpt  43113  ndmaovcl  43409  ndmaovcom  43411  ndmaovass  43412  ndmaovdistr  43413  dfatco  43462  otiunsndisjX  43485  fvmptrabdm  43499  elsetpreimafvb  43551  sprsymrelfolem2  43662  sprsymrelf  43664  sprsymrelf1  43665  prpair  43670  prproropf1olem0  43671  paireqne  43680  fmtno4prmfac  43741  dfodd5  43832  sbgoldbo  43959  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  isomushgr  43998  isomuspgrlem2c  44002  uspgrsprf  44028  uspgrsprf1  44029  uspgrsprfo  44030  opeliun2xp  44388  ply1sclrmsm  44444  lcoop  44473  lincfsuppcl  44475  linccl  44476  lincvalsng  44478  lincvalpr  44480  lincvalsc0  44483  linc0scn0  44485  lincdifsn  44486  linc1  44487  lincsum  44491  lincscm  44492  lspsslco  44499  snlindsntor  44533  lincresunit3lem2  44542  ldepsnlinclem1  44567  ldepsnlinclem2  44568  prelrrx2  44707  prelrrx2b  44708  rrx2xpref1o  44712  rrx2plord  44714  rrx2linesl  44737  elpglem3  44822