Theorem eleq2i 2904

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 2901	. 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 2793

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

This theorem is referenced by:  eleq12i  2905  eleqtri  2911  eleq2s  2931  hbxfreq  2942  nfceqi  2973  raleqbii  3234  rexeqbii  3326  rabeq2i  3487  elab2g  3668  elrabf  3676  elrab3t  3679  elrab2  3683  cbvsbcw  3804  cbvsbc  3806  elin2  4174  elsymdif  4224  dfnul2OLD  4294  noel  4296  noelOLD  4297  eltpg  4623  elunirab  4854  elintrab  4888  disjxiun  5063  exss  5355  otiunsndisj  5410  brabsb  5418  brabga  5421  epelg  5466  pofun  5491  elxp  5578  opeliunxp  5619  bropaex12  5642  brab2a  5644  elcnv  5747  dmopabelb  5785  elrnmptg  5831  elres  5891  elrid  5913  rninxp  6036  elid  6056  elsuci  6257  elsucg  6258  elsuc2g  6259  elfv  6668  0fv  6709  opabiota  6746  dffv2  6756  fvopab3g  6763  fvmptex  6782  fvopab5  6800  fvn0ssdmfun  6842  fveqressseq  6847  f0cli  6864  fmptco  6891  fvrnressn  6923  funfvima  6992  elunirnALT  7011  fliftel  7062  eloprabga  7261  elrnmpo  7287  ovid  7291  offval  7416  suceloni  7528  1st2val  7717  2nd2val  7718  bropopvvv  7785  bropfvvvv  7787  fsplit  7812  fsplitOLD  7813  xporderlem  7821  brtpos2  7898  wfrdmcl  7963  wfrfun  7965  wfrlem12  7966  wfrlem17  7971  wfr2  7974  issmo  7985  smores3  7990  tfrlem7  8019  tfrlem9  8021  tfrlem9a  8022  tfr2b  8032  tfr2  8034  rdgsuc  8060  frsucmptn  8074  tz7.48-2  8078  el1o  8124  dif1o  8125  ondif2  8127  oawordeulem  8180  elecg  8332  brecop  8390  erovlem  8393  eceqoveq  8402  mapsncnv  8457  mptelixpg  8499  brsdom  8532  isfi  8533  enssdom  8534  brdom2  8539  xpcomco  8607  brsdom2  8641  en3lplem2  9076  cnfcom2lem  9164  epfrs  9173  r1limg  9200  r1ord  9209  r1ord3  9211  tz9.12lem3  9218  rankvaln  9228  r1elss  9235  rankpwi  9252  ssrankr1  9264  r1val3  9267  r1pw  9274  rankr1b  9293  djur  9348  djuunxp  9350  eldju2ndl  9353  eldju2ndr  9354  isnum2  9374  cardprclem  9408  infxpenlem  9439  alephcard  9496  alephnbtwn  9497  alephnbtwn2  9498  alephord2  9502  alephsdom  9512  dfac3  9547  dfac5lem2  9550  dfac5lem3  9551  dfac5lem5  9553  pwsdompw  9626  cfub  9671  cardcf  9674  cflecard  9675  cfle  9676  cflim2  9685  cofsmo  9691  cfidm  9697  isfin3  9718  isfin5  9721  isfin6  9722  sdom2en01  9724  fin23lem26  9747  fin23lem30  9764  isf32lem5  9779  itunitc1  9842  ituniiun  9844  axdc3lem3  9874  axcclem  9879  axdclem  9941  iunfo  9961  iundom2g  9962  cardidg  9970  konigthlem  9990  alephadd  9999  alephreg  10004  pwcfsdom  10005  cfpwsdom  10006  elgch  10044  fpwwe2lem12  10063  canth4  10069  wunex2  10160  r1tskina  10204  elni  10298  nlt1pi  10328  adderpq  10378  mulerpq  10379  recmulnq  10386  addsrpr  10497  mulsrpr  10498  opelcn  10551  opelreal  10552  elreal  10553  elreal2  10554  0ncn  10555  addcnsr  10557  mulcnsr  10558  xrlenlt  10706  elnn0  11900  elnnne0  11912  un0addcl  11931  un0mulcl  11932  elxnn0  11970  uztrn2  12263  elnnuz  12283  elnn0uz  12284  elq  12351  elxr  12512  elfzm1b  12986  elfz0lmr  13153  uzrdgfni  13327  fzennn  13337  ser0  13423  hash2pwpr  13835  iswrd  13864  pfxccatpfx1  14098  s3iunsndisj  14328  sumz  15079  sumss  15081  fsumcvg3  15086  abscvgcvg  15174  isumshft  15194  prodf1  15247  zprod  15291  prod1  15298  prodss  15301  prodsn  15316  prodsnf  15318  bpolydiflem  15408  bpoly2  15411  bpoly3  15412  bpoly4  15413  ruclem6  15588  divides  15609  dvdsflip  15667  pwp1fsum  15742  sadc0  15803  eulerthlem2  16119  prm23lt5  16151  4sqlem2  16285  4sqlem12  16292  vdwpc  16316  xpscf  16838  cidpropd  16980  oppcsect  17048  funcpropd  17170  natpropd  17246  initoeu2lem0  17273  arwhoma  17305  eldmcoa  17325  pospo  17583  psss  17824  ismgmn0  17854  gsumpropd2lem  17889  elefmndbas  18038  smndex1basss  18070  smndex1mgm  18072  pwmnd  18102  dfgrp2e  18129  mulgfval  18226  cycsubmel  18343  ghmeqker  18385  cntri  18461  oppgsubg  18491  fvcosymgeq  18557  symgfixels  18562  pmtrfrn  18586  efgsfo  18865  efgrelexlemb  18876  lt6abl  19015  dmdprd  19120  dprdval  19125  dprdw  19132  srgbinomlem4  19293  isnirred  19450  isrhm  19473  issrng  19621  lspexchn2  19903  lspindp2l  19906  lspindp2  19907  lbsextlem2  19931  evlslem4  20288  ply1bascl2  20372  cply1mul  20462  lply1binom  20474  cnfldfunALT  20558  dsmmelbas  20883  frlmbas3  20920  lindsind2  20963  islindf4  20982  matsubgcell  21043  matinvgcell  21044  matvscacell  21045  matepmcl  21071  matepm2cl  21072  scmatscm  21122  smatvscl  21133  marrepcl  21173  marepvcl  21178  mulmarep1el  21181  mulmarep1gsum1  21182  mulmarep1gsum2  21183  submabas  21187  m1detdiag  21206  mdetdiag  21208  m2detleib  21240  gsummatr01lem3  21266  gsummatr01  21268  smadiadetlem4  21278  slesolinv  21289  slesolinvbi  21290  slesolex  21291  cramerimplem2  21293  pmatcoe1fsupp  21309  mat2pmatbas  21334  mat2pmatmul  21339  mat2pmatlin  21343  decpmatmul  21380  monmatcollpw  21387  pm2mpf1  21407  pm2mpghm  21424  istps  21542  mretopd  21700  neiptopuni  21738  lpdifsn  21751  restcls  21789  perfopn  21793  pnfnei  21828  mnfnei  21829  lmss  21906  hauscmplem  22014  is2ndc  22054  2ndcdisj  22064  hausnlly  22101  txuni2  22173  ptpjpre1  22179  elpt  22180  dfac14  22226  xkococn  22268  fbasrn  22492  fin1aufil  22540  elfm2  22556  elfm3  22558  fbflim  22584  flffbas  22603  cnpflf2  22608  fclsbas  22629  efmndtmd  22709  tsmssubm  22751  iscusp2  22911  imasdsf1olem  22983  metustel  23160  metuel2  23175  isnghm  23332  opnreen  23439  iccpnfcnv  23548  ehleudisval  24022  ehl1eudis  24023  ehl2eudis  24025  minveclem3b  24031  ovoliunlem1  24103  ioombl1lem4  24162  subopnmbl  24205  vitalilem2  24210  vitalilem3  24211  mbfimaopnlem  24256  mbfimaopn2  24258  itg2l  24330  dvply1  24873  vieta1lem1  24899  vieta1lem2  24900  elaa  24905  taylthlem2  24962  abelthlem6  25024  abelthlem9  25028  sinq34lt0t  25095  ellogrn  25143  dvrelog  25220  ellogdm  25222  logtayl2  25245  cxpcn3lem  25328  cxpcn3  25329  1cubr  25420  atandm  25454  atanf  25458  reasinsin  25474  atans2  25509  dmarea  25535  xrlimcnp  25546  amgmlem  25567  ppiublem1  25778  lgsdir2lem2  25902  gausslemma2dlem1a  25941  lgsquadlem1  25956  lgsquadlem2  25957  2sqlem1  25993  rpvmasum2  26088  edgiedgb  26839  isuhgr  26845  isushgr  26846  isupgr  26869  isumgr  26880  umgredg  26923  umgrpredgv  26925  umgredgne  26930  umgredgnlp  26932  isuspgr  26937  isusgr  26938  ausgrusgri  26953  usgredgppr  26978  edgssv2  26980  uspgredg2vlem  27005  uspgredg2v  27006  ushgredgedg  27011  ushgredgedgloop  27013  griedg0ssusgr  27047  uhgrissubgr  27057  subumgredg2  27067  uhgrspansubgrlem  27072  umgrres1lem  27092  upgrres1  27095  nbgrcl  27117  nbuhgr  27125  nbuhgr2vtx1edgblem  27133  nbupgrres  27146  edgnbusgreu  27149  nbusgredgeu0  27150  nbusgrf1o0  27151  hashnbusgrnn0  27158  nbupgruvtxres  27189  cffldtocusgr  27229  cusgrfilem2  27238  vtxdg0v  27255  vtxduhgr0nedg  27274  uhgrvd00  27316  vtxdginducedm1  27325  finsumvtxdg2ssteplem4  27330  wlk1walk  27420  wlkp1lem6  27460  iswwlks  27614  wwlknllvtx  27624  wwlksonvtx  27633  wspthnonp  27637  wlkiswwlksupgr2  27655  wwlksnwwlksnon  27694  2pthon3v  27722  umgr2wlk  27728  elwwlks2s3  27730  wwlks2onv  27732  elwwlks2ons3im  27733  isclwwlk  27762  clwwlkccatlem  27767  clwlkclwwlk  27780  wwlksext2clwwlk  27836  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknon1  27876  clwwlknon1nloop  27878  clwwlknon2x  27882  1pthon2v  27932  uhgr3cyclex  27961  isconngr  27968  isconngr1  27969  eucrctshift  28022  frgrnbnb  28072  frgrncvvdeqlem1  28078  frgrncvvdeqlem2  28079  frgrncvvdeqlem3  28080  frgrncvvdeqlem9  28086  fusgreghash2wspv  28114  extwwlkfab  28131  numclwwlk1lem2foa  28133  numclwwlk1lem2fo  28137  clwlknon2num  28147  numclwlk2lem2f1o  28158  numclwwlk5lem  28166  topnfbey  28248  isvclem  28354  isnvlem  28387  vsfval  28410  h2hlm  28757  hhcmpl  28977  hhcms  28980  elch0  29031  omlsilem  29179  h1de2ctlem  29332  elspansni  29335  nonbooli  29428  spansncvi  29429  adjeq  29712  cnlnssadj  29857  cnvbraval  29887  brabgaf  30359  elimampt  30383  fmptdF  30401  fmptcof2  30402  acunirnmpt  30404  acunirnmpt2  30405  ofpreima  30410  fcnvgreu  30418  1stpreima  30442  2ndpreima  30443  fz2ssnn0  30508  elxrge02  30608  psgnfzto1stlem  30742  cycpmgcl  30795  submatres  31071  lmat22lem  31082  crefdf  31112  cmppcmp  31122  prsdm  31157  prsrn  31158  xrge0iifcnv  31176  xrge0iifiso  31178  xrge0iifhom  31180  pnfneige0  31194  qqhre  31261  rrhre  31262  esumnul  31307  esumcvgsum  31347  ldgenpisyslem1  31422  measvuni  31473  cntnevol  31487  dya2iocnrect  31539  sibf0  31592  oddpwdc  31612  eulerpartlemd  31624  eulerpartgbij  31630  eulerpartlemgh  31636  isrrvv  31701  coinfliprv  31740  ballotlem7  31793  signswch  31831  hashreprin  31891  chtvalz  31900  circlemethhgt  31914  hgt750lemb  31927  tgoldbachgt  31934  bnj23  31988  bnj158  31999  bnj168  32000  bnj1138  32060  bnj1143  32062  bnj1454  32114  bnj110  32130  bnj882  32198  bnj893  32200  bnj916  32205  bnj970  32219  bnj983  32223  bnj984  32224  bnj1137  32267  bnj1174  32275  bnj1388  32305  bnj1398  32306  loop1cycl  32384  subfacp1lem5  32431  satfv1  32610  satfrnmapom  32617  satf0op  32624  satf0n0  32625  fmlafvel  32632  fmlaomn0  32637  fmlan0  32638  satffunlem2lem2  32653  satfv0fvfmla0  32660  satefvfmla0  32665  mrsub0  32763  mrsubccat  32765  mrsubcn  32766  elmrsubrn  32767  msubco  32778  msubvrs  32807  elmthm  32823  mthmblem  32827  elrn3  32998  dfon2lem7  33034  eltrpred  33065  frrlem8  33130  frrlem9  33131  frrlem10  33132  madeval2  33290  brsset  33350  eltrans  33352  elfix  33364  ellimits  33371  elfuns  33376  elsingles  33379  fvtransport  33493  brcolinear2  33519  fvray  33602  linedegen  33604  fvline  33605  ellines  33613  fwddifn0  33625  elhf  33635  hfninf  33647  fnessref  33705  bj-ififc  33915  bj-csbsnlem  34223  currysetlem1  34261  bj-eltag  34292  bj-sngltag  34298  bj-projun  34309  bj-0nelmpt  34411  bj-opelidres  34456  bj-inftyexpitaudisj  34490  bj-elccinfty  34499  f1omptsnlem  34620  icoreelrnab  34638  relowlpssretop  34648  rdgssun  34662  exrecfnlem  34663  finxpnom  34685  uncov  34888  tan2h  34899  ptrecube  34907  poimirlem25  34932  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  cnambfre  34955  ftc1cnnc  34981  sdclem2  35032  sdclem1  35033  fdc  35035  caushft  35051  issmgrpOLD  35156  ismndo  35165  isrngo  35190  isdivrngo  35243  csbcom2fi  35421  elecALTV  35542  brrabga  35613  eldmcoss  35713  coss0  35734  elrels2  35741  dath  36887  diclspsn  38345  dvh4dimlem  38594  dvh2dim  38596  dvh3dim3N  38600  lcfrvalsnN  38692  mapdh6eN  38891  mapdh7dN  38901  mapdh8b  38931  hdmap1l6e  38965  lcmfunnnd  39133  frlmfielbas  39188  pellex  39481  rmspecnonsq  39553  islmodfg  39718  aaitgo  39811  areaquad  39872  elcnvcnvintab  39991  elnonrel  39994  elcnvcnvlem  40008  cnvcnvintabd  40009  brfvrcld2  40086  grur1cld  40617  dvgrat  40693  cvgdvgrat  40694  radcnvrat  40695  nznngen  40697  uzmptshftfval  40727  binomcxplemcvg  40735  binomcxplemnotnn0  40737  tpid3gVD  41225  en3lplem2VD  41227  rexanuz3  41411  eliuniin  41414  eliuniin2  41435  disjinfi  41503  fsneq  41518  iuneqfzuzlem  41651  allbutfi  41714  eluzelz2  41725  uz0  41735  uzublem  41753  uzid3  41758  elicores  41858  uzinico  41885  climsuselem1  41937  climsuse  41938  islptre  41949  fnlimfvre  42004  limsupresico  42030  limsupvaluz  42038  limsupubuzlem  42042  limsupequzmptlem  42058  liminfresico  42101  cnrefiisplem  42159  stoweidlem14  42348  stoweidlem39  42373  stoweidlem48  42382  stoweidlem51  42385  stoweidlem59  42393  stoweidlem62  42396  wallispilem3  42401  fourierdlem42  42483  fourierdlem62  42502  fourierdlem80  42520  fourierdlem103  42543  fourierdlem104  42544  etransclem26  42594  rrxsnicc  42634  ioorrnopn  42639  ioorrnopnxr  42641  sge00  42707  sge0fodjrnlem  42747  sge0isum  42758  sge0seq  42777  meadjiunlem  42796  carageneld  42833  volicorescl  42884  hoidmv1lelem1  42922  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem3  42928  ovnhoilem2  42933  hoiqssbllem2  42954  opnvonmbllem2  42964  ovolval4lem1  42980  iinhoiicc  43005  vonioolem1  43011  smflimlem1  43096  smflimlem2  43097  smflim  43102  nsssmfmbf  43104  smfresal  43112  smfrec  43113  smfdiv  43121  smfpimbor1lem2  43123  smflim2  43129  smflimmpt  43133  smfsupmpt  43138  smfinflem  43140  smfinfmpt  43142  smflimsuplem1  43143  smflimsuplem2  43144  smflimsuplem3  43145  smflimsuplem5  43147  smflimsuplem6  43148  smflimsup  43151  smflimsupmpt  43152  smfliminfmpt  43155  ndmaovcl  43451  ndmaovcom  43453  ndmaovass  43454  ndmaovdistr  43455  dfatco  43504  otiunsndisjX  43527  fvmptrabdm  43541  elsetpreimafvb  43593  sprsymrelfolem2  43704  sprsymrelf  43706  sprsymrelf1  43707  prpair  43712  prproropf1olem0  43713  paireqne  43722  fmtno4prmfac  43783  dfodd5  43874  sbgoldbo  44001  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  isomushgr  44040  isomuspgrlem2c  44044  uspgrsprf  44070  uspgrsprf1  44071  uspgrsprfo  44072  opeliun2xp  44430  ply1sclrmsm  44486  lcoop  44515  lincfsuppcl  44517  linccl  44518  lincvalsng  44520  lincvalpr  44522  lincvalsc0  44525  linc0scn0  44527  lincdifsn  44528  linc1  44529  lincsum  44533  lincscm  44534  lspsslco  44541  snlindsntor  44575  lincresunit3lem2  44584  ldepsnlinclem1  44609  ldepsnlinclem2  44610  prelrrx2  44749  prelrrx2b  44750  rrx2xpref1o  44754  rrx2plord  44756  rrx2linesl  44779  elpglem3  44864