Theorem eleq2i 2872

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

Syntax hints:   ↔ wb 207   = wceq 1520   ∈ wcel 2079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-clel 2861

This theorem is referenced by:  eleq12i  2873  eleqtri  2879  eleq2s  2899  hbxfreq  2910  nfceqi  2943  raleqbii  3196  rexeqbii  3284  rabeq2i  3427  elab2g  3602  elrabf  3609  elrab3t  3612  elrab2  3616  cbvsbc  3730  elin2  4090  elsymdif  4139  dfnul2OLD  4209  noel  4211  noelOLD  4212  eltpg  4524  elunirab  4751  elintrab  4788  disjxiun  4953  exss  5240  otiunsndisj  5294  brabsb  5300  brabga  5303  epelg  5346  pofun  5371  elxp  5458  opeliunxp  5497  bropaex12  5520  brab2a  5522  elcnv  5625  dmopabelb  5663  elrnmptg  5705  elres  5764  elrid  5786  rninxp  5904  elid  5923  elsuci  6124  elsucg  6125  elsuc2g  6126  elfv  6528  0fv  6569  opabiota  6605  dffv2  6615  fvopab3g  6621  fvmptex  6639  fvopab5  6656  fvn0ssdmfun  6698  fveqressseq  6703  f0cli  6718  fmptco  6745  fvrnressn  6777  funfvima  6849  elunirnALT  6867  fliftel  6916  eloprabga  7108  elrnmpo  7134  ovid  7138  offval  7265  suceloni  7375  1st2val  7564  2nd2val  7565  bropopvvv  7632  bropfvvvv  7634  fsplit  7659  xporderlem  7665  brtpos2  7740  wfrdmcl  7806  wfrfun  7808  wfrlem12  7809  wfrlem17  7814  wfr2  7817  issmo  7828  smores3  7833  tfrlem7  7862  tfrlem9  7864  tfrlem9a  7865  tfr2b  7875  tfr2  7877  rdgsuc  7903  frsucmptn  7917  tz7.48-2  7920  el1o  7966  dif1o  7967  ondif2  7969  oawordeulem  8021  elecg  8173  brecop  8231  erovlem  8234  eceqoveq  8243  mapsncnv  8296  mptelixpg  8337  brsdom  8370  isfi  8371  enssdom  8372  brdom2  8377  xpcomco  8444  brsdom2  8478  en3lplem2  8911  cnfcom2lem  8999  epfrs  9008  r1limg  9035  r1ord  9044  r1ord3  9046  tz9.12lem3  9053  rankvaln  9063  r1elss  9070  rankpwi  9087  ssrankr1  9099  r1val3  9102  r1pw  9109  rankr1b  9128  djur  9183  djuunxp  9185  eldju2ndl  9188  eldju2ndr  9189  isnum2  9209  cardprclem  9243  infxpenlem  9274  alephcard  9331  alephnbtwn  9332  alephnbtwn2  9333  alephord2  9337  alephsdom  9347  dfac3  9382  dfac5lem2  9385  dfac5lem3  9386  dfac5lem5  9388  pwsdompw  9461  cfub  9506  cardcf  9509  cflecard  9510  cfle  9511  cflim2  9520  cofsmo  9526  cfidm  9532  isfin3  9553  isfin5  9556  isfin6  9557  sdom2en01  9559  fin23lem26  9582  fin23lem30  9599  isf32lem5  9614  itunitc1  9677  ituniiun  9679  axdc3lem3  9709  axcclem  9714  axdclem  9776  iunfo  9796  iundom2g  9797  cardidg  9805  konigthlem  9825  alephadd  9834  alephreg  9839  pwcfsdom  9840  cfpwsdom  9841  elgch  9879  fpwwe2lem12  9898  canth4  9904  wunex2  9995  r1tskina  10039  elni  10133  nlt1pi  10163  adderpq  10213  mulerpq  10214  recmulnq  10221  addsrpr  10332  mulsrpr  10333  opelcn  10386  opelreal  10387  elreal  10388  elreal2  10389  0ncn  10390  addcnsr  10392  mulcnsr  10393  xrlenlt  10542  elnn0  11736  elnnne0  11748  un0addcl  11767  un0mulcl  11768  elxnn0  11806  uztrn2  12100  elnnuz  12120  elnn0uz  12121  elq  12188  elxr  12350  elfzm1b  12824  elfz0lmr  12990  uzrdgfni  13164  fzennn  13174  ser0  13260  hash2pwpr  13668  iswrd  13697  pfxccatpfx1  13922  s3iunsndisj  14150  sumz  14900  sumss  14902  fsumcvg3  14907  abscvgcvg  14995  isumshft  15015  prodf1  15068  zprod  15112  prod1  15119  prodss  15122  prodsn  15137  prodsnf  15139  bpolydiflem  15229  bpoly2  15232  bpoly3  15233  bpoly4  15234  ruclem6  15409  divides  15430  dvdsflip  15488  pwp1fsum  15563  sadc0  15624  eulerthlem2  15936  prm23lt5  15968  4sqlem2  16102  4sqlem12  16109  vdwpc  16133  xpscf  16655  cidpropd  16797  oppcsect  16865  funcpropd  16987  natpropd  17063  initoeu2lem0  17090  arwhoma  17122  eldmcoa  17142  pospo  17400  psss  17641  ismgmn0  17671  gsumpropd2lem  17700  dfgrp2e  17875  mulgfval  17971  ghmeqker  18114  cntri  18190  oppgsubg  18220  fvcosymgeq  18276  symgfixels  18281  pmtrfrn  18305  efgsfo  18580  efgrelexlemb  18591  lt6abl  18724  dmdprd  18825  dprdval  18830  dprdw  18837  srgbinomlem4  18971  isnirred  19128  isrhm  19151  issrng  19299  lspexchn2  19581  lspindp2l  19584  lspindp2  19585  lbsextlem2  19609  evlslem4  19963  ply1bascl2  20043  cply1mul  20133  lply1binom  20145  cnfldfunALT  20228  dsmmelbas  20553  frlmbas3  20590  lindsind2  20633  islindf4  20652  matsubgcell  20715  matinvgcell  20716  matvscacell  20717  matepmcl  20743  matepm2cl  20744  scmatscm  20794  smatvscl  20805  marrepcl  20845  marepvcl  20850  mulmarep1el  20853  mulmarep1gsum1  20854  mulmarep1gsum2  20855  submabas  20859  m1detdiag  20878  mdetdiag  20880  m2detleib  20912  gsummatr01lem3  20938  gsummatr01  20940  smadiadetlem4  20950  slesolinv  20961  slesolinvbi  20962  slesolex  20963  cramerimplem2  20965  pmatcoe1fsupp  20981  mat2pmatbas  21006  mat2pmatmul  21011  mat2pmatlin  21015  decpmatmul  21052  monmatcollpw  21059  pm2mpf1  21079  pm2mpghm  21096  istps  21214  mretopd  21372  neiptopuni  21410  lpdifsn  21423  restcls  21461  perfopn  21465  pnfnei  21500  mnfnei  21501  lmss  21578  hauscmplem  21686  is2ndc  21726  2ndcdisj  21736  hausnlly  21773  txuni2  21845  ptpjpre1  21851  elpt  21852  dfac14  21898  xkococn  21940  fbasrn  22164  fin1aufil  22212  elfm2  22228  elfm3  22230  fbflim  22256  flffbas  22275  cnpflf2  22280  fclsbas  22301  tsmssubm  22422  iscusp2  22582  imasdsf1olem  22654  metustel  22831  metuel2  22846  isnghm  23003  opnreen  23110  iccpnfcnv  23219  ehleudisval  23693  ehl1eudis  23694  ehl2eudis  23696  minveclem3b  23702  ovoliunlem1  23774  ioombl1lem4  23833  subopnmbl  23876  vitalilem2  23881  vitalilem3  23882  mbfimaopnlem  23927  mbfimaopn2  23929  itg2l  24001  dvply1  24544  vieta1lem1  24570  vieta1lem2  24571  elaa  24576  taylthlem2  24633  abelthlem6  24695  abelthlem9  24699  sinq34lt0t  24766  ellogrn  24812  dvrelog  24889  ellogdm  24891  logtayl2  24914  cxpcn3lem  24997  cxpcn3  24998  1cubr  25089  atandm  25123  atanf  25127  reasinsin  25143  atans2  25178  dmarea  25205  xrlimcnp  25216  amgmlem  25237  ppiublem1  25448  lgsdir2lem2  25572  gausslemma2dlem1a  25611  lgsquadlem1  25626  lgsquadlem2  25627  2sqlem1  25663  rpvmasum2  25758  edgiedgb  26510  isuhgr  26516  isushgr  26517  isupgr  26540  isumgr  26551  umgredg  26594  umgrpredgv  26596  umgredgne  26601  umgredgnlp  26603  isuspgr  26608  isusgr  26609  ausgrusgri  26624  usgredgppr  26649  edgssv2  26651  uspgredg2vlem  26676  uspgredg2v  26677  ushgredgedg  26682  ushgredgedgloop  26684  griedg0ssusgr  26718  uhgrissubgr  26728  subumgredg2  26738  uhgrspansubgrlem  26743  umgrres1lem  26763  upgrres1  26766  nbgrcl  26788  nbuhgr  26796  nbuhgr2vtx1edgblem  26804  nbupgrres  26817  edgnbusgreu  26820  nbusgredgeu0  26821  nbusgrf1o0  26822  hashnbusgrnn0  26829  nbupgruvtxres  26860  cffldtocusgr  26900  cusgrfilem2  26909  vtxdg0v  26926  vtxduhgr0nedg  26945  uhgrvd00  26987  vtxdginducedm1  26996  finsumvtxdg2ssteplem4  27001  wlk1walk  27091  wlkp1lem6  27133  iswwlks  27289  wwlknllvtx  27299  wwlksonvtx  27308  wspthnonp  27312  wlkiswwlksupgr2  27330  wwlksnwwlksnon  27369  2pthon3v  27397  umgr2wlk  27403  elwwlks2s3  27405  wwlks2onv  27407  elwwlks2ons3im  27408  isclwwlk  27437  clwwlkccatlem  27442  clwlkclwwlk  27455  wwlksext2clwwlk  27511  hashecclwwlkn1  27531  umgrhashecclwwlk  27532  clwwlknon1  27551  clwwlknon1nloop  27553  clwwlknon2x  27557  1pthon2v  27607  uhgr3cyclex  27636  isconngr  27643  isconngr1  27644  eucrctshift  27698  isfrgr  27717  frgrnbnb  27752  frgrncvvdeqlem1  27758  frgrncvvdeqlem2  27759  frgrncvvdeqlem3  27760  frgrncvvdeqlem9  27766  fusgreghash2wspv  27794  extwwlkfab  27811  numclwwlk1lem2foa  27813  numclwwlk1lem2fo  27817  clwlknon2num  27827  numclwlk2lem2f1o  27838  numclwwlk5lem  27846  topnfbey  27927  isvclem  28033  isnvlem  28066  vsfval  28089  h2hlm  28436  hhcmpl  28656  hhcms  28659  elch0  28710  omlsilem  28858  h1de2ctlem  29011  elspansni  29014  nonbooli  29107  spansncvi  29108  adjeq  29391  cnlnssadj  29536  cnvbraval  29566  brabgaf  30024  elimampt  30046  fmptdF  30064  fmptcof2  30065  acunirnmpt  30067  acunirnmpt2  30068  ofpreima  30073  fcnvgreu  30081  1stpreima  30103  2ndpreima  30104  fz2ssnn0  30168  elxrge02  30263  cycpmgcl  30391  psgnfzto1stlem  30620  submatres  30642  lmat22lem  30653  crefdf  30685  cmppcmp  30695  prsdm  30730  prsrn  30731  xrge0iifcnv  30749  xrge0iifiso  30751  xrge0iifhom  30753  pnfneige0  30767  qqhre  30834  rrhre  30835  esumnul  30880  esumcvgsum  30920  ldgenpisyslem1  30995  measvuni  31046  cntnevol  31060  dya2iocnrect  31112  sibf0  31165  oddpwdc  31185  eulerpartlemd  31197  eulerpartgbij  31203  eulerpartlemgh  31209  isrrvv  31274  coinfliprv  31313  ballotlem7  31366  signswch  31404  hashreprin  31464  chtvalz  31473  circlemethhgt  31487  hgt750lemb  31500  tgoldbachgt  31507  bnj23  31561  bnj158  31572  bnj168  31573  bnj1138  31633  bnj1143  31635  bnj1454  31686  bnj110  31702  bnj882  31770  bnj893  31772  bnj916  31777  bnj970  31791  bnj983  31795  bnj984  31796  bnj1137  31837  bnj1174  31845  bnj1388  31875  bnj1398  31876  loop1cycl  31948  subfacp1lem5  31995  satfrnmapom  32179  satf0op  32186  satf0n0  32187  fmlafvel  32194  fmlan0  32199  satffunlem2lem2  32214  satfv0fvfmla0  32221  satefvfmla0  32226  mrsub0  32316  mrsubccat  32318  mrsubcn  32319  elmrsubrn  32320  msubco  32331  msubvrs  32360  elmthm  32376  mthmblem  32380  elrn3  32551  dfon2lem7  32587  eltrpred  32619  frrlem8  32684  frrlem9  32685  frrlem10  32686  madeval2  32844  brsset  32904  eltrans  32906  elfix  32918  ellimits  32925  elfuns  32930  elsingles  32933  fvtransport  33047  brcolinear2  33073  fvray  33156  linedegen  33158  fvline  33159  ellines  33167  fwddifn0  33179  elhf  33189  hfninf  33201  fnessref  33259  bj-csbsnlem  33735  currysetlem1  33775  bj-eltag  33840  bj-sngltag  33846  bj-projun  33857  bj-0nelmpt  33952  bj-elid  33973  bj-inftyexpitaudisj  33991  bj-elccinfty  34000  f1omptsnlem  34094  icoreelrnab  34112  relowlpssretop  34122  rdgssun  34136  exrecfnlem  34137  finxpnom  34159  uncov  34350  tan2h  34361  ptrecube  34369  poimirlem25  34394  poimirlem29  34398  poimirlem30  34399  poimirlem31  34400  poimirlem32  34401  cnambfre  34417  ftc1cnnc  34443  sdclem2  34495  sdclem1  34496  fdc  34498  caushft  34514  issmgrpOLD  34619  ismndo  34628  isrngo  34653  isdivrngo  34706  csbcom2fi  34886  elecALTV  35007  brrabga  35080  eldmcoss  35179  coss0  35200  elrels2  35207  dath  36353  diclspsn  37811  dvh4dimlem  38060  dvh2dim  38062  dvh3dim3N  38066  lcfrvalsnN  38158  mapdh6eN  38357  mapdh7dN  38367  mapdh8b  38397  hdmap1l6e  38431  frlmfielbas  38616  pellex  38868  rmspecnonsq  38940  islmodfg  39105  aaitgo  39198  areaquad  39259  elcnvcnvintab  39378  elnonrel  39381  elcnvcnvlem  39395  cnvcnvintabd  39396  brfvrcld2  39473  grur1cld  40017  dvgrat  40134  cvgdvgrat  40135  radcnvrat  40136  nznngen  40138  uzmptshftfval  40168  binomcxplemcvg  40176  binomcxplemnotnn0  40178  tpid3gVD  40667  en3lplem2VD  40669  rexanuz3  40854  eliuniin  40857  eliuniin2  40879  disjinfi  40947  fsneq  40962  iuneqfzuzlem  41096  allbutfi  41160  eluzelz2  41171  uz0  41182  uzublem  41200  uzid3  41205  elicores  41305  uzinico  41332  climsuselem1  41384  climsuse  41385  islptre  41396  fnlimfvre  41451  limsupresico  41477  limsupvaluz  41485  limsupubuzlem  41489  limsupequzmptlem  41505  liminfresico  41548  cnrefiisplem  41606  stoweidlem14  41795  stoweidlem39  41820  stoweidlem48  41829  stoweidlem51  41832  stoweidlem59  41840  stoweidlem62  41843  wallispilem3  41848  fourierdlem42  41930  fourierdlem62  41949  fourierdlem80  41967  fourierdlem103  41990  fourierdlem104  41991  etransclem26  42041  rrxsnicc  42081  ioorrnopn  42086  ioorrnopnxr  42088  sge00  42154  sge0fodjrnlem  42194  sge0isum  42205  sge0seq  42224  meadjiunlem  42243  carageneld  42280  volicorescl  42331  hoidmv1lelem1  42369  hoidmv1le  42372  hoidmvlelem1  42373  hoidmvlelem3  42375  ovnhoilem2  42380  hoiqssbllem2  42401  opnvonmbllem2  42411  ovolval4lem1  42427  iinhoiicc  42452  vonioolem1  42458  smflimlem1  42543  smflimlem2  42544  smflim  42549  nsssmfmbf  42551  smfresal  42559  smfrec  42560  smfdiv  42568  smfpimbor1lem2  42570  smflim2  42576  smflimmpt  42580  smfsupmpt  42585  smfinflem  42587  smfinfmpt  42589  smflimsuplem1  42590  smflimsuplem2  42591  smflimsuplem3  42592  smflimsuplem5  42594  smflimsuplem6  42595  smflimsup  42598  smflimsupmpt  42599  smfliminfmpt  42602  ndmaovcl  42872  ndmaovcom  42874  ndmaovass  42875  ndmaovdistr  42876  dfatco  42925  otiunsndisjX  42948  fvmptrabdm  42962  sprsymrelfolem2  43091  sprsymrelf  43093  sprsymrelf1  43094  prpair  43099  prproropf1olem0  43100  paireqne  43109  fmtno4prmfac  43170  dfodd5  43261  sbgoldbo  43388  nnsum4primeseven  43401  nnsum4primesevenALTV  43402  isomushgr  43427  isomuspgrlem2c  43431  uspgrsprf  43457  uspgrsprf1  43458  uspgrsprfo  43459  opeliun2xp  43813  ply1sclrmsm  43871  lcoop  43900  lincfsuppcl  43902  linccl  43903  lincvalsng  43905  lincvalpr  43907  lincvalsc0  43910  linc0scn0  43912  lincdifsn  43913  linc1  43914  lincsum  43918  lincscm  43919  lspsslco  43926  snlindsntor  43960  lincresunit3lem2  43969  ldepsnlinclem1  43994  ldepsnlinclem2  43995  prelrrx2  44135  prelrrx2b  44136  rrx2xpref1o  44140  rrx2plord  44142  rrx2linesl  44165  elpglem3  44249