Theorem eleq2i 2298

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq2i	⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq2 2295	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 105   = wceq 1397   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12i  2299  eleqtri  2306  eleq2s  2326  hbxfreq  2338  abeq2i  2342  abeq1i  2343  nfceqi  2370  raleqbii  2544  rexeqbii  2545  rabeq2i  2799  elab2g  2953  elrabf  2960  elrab3t  2961  elrab2  2965  cbvsbcw  3059  cbvsbc  3060  csbcow  3138  elin2  3395  dfnul2  3496  noel  3498  rabn0m  3522  rabeq0  3524  eltpg  3714  tpid3g  3787  oprcl  3886  elunirab  3906  elintrab  3940  exss  4319  elop  4323  opm  4326  brabsb  4355  brabga  4358  pofun  4409  elsuci  4500  elsucg  4501  elsuc2g  4502  ordsucim  4598  peano2  4693  elxp  4742  brab2a  4779  brab2ga  4801  elco  4896  elcnv  4907  dmmrnm  4951  elrnmptg  4984  opelres  5018  rninxp  5180  eliota  5314  funco  5366  elfv  5637  nfvres  5675  fvopab3g  5719  fvmptssdm  5731  fmptco  5813  funfvima  5885  fliftel  5933  acexmidlema  6008  acexmidlemb  6009  acexmidlem2  6014  eloprabga  6107  elrnmpo  6134  ovid  6137  offval  6242  xporderlem  6395  brtpos2  6416  issmo  6453  smores3  6458  tfrlem7  6482  tfrlem9  6484  tfr0dm  6487  tfri2  6531  rdgon  6551  freccllem  6567  frecfcllem  6569  frecsuclem  6571  el1o  6604  dif1o  6605  nnsucuniel  6662  elecg  6741  brecop  6793  erovlem  6795  oviec  6809  mapsncnv  6863  mptelixpg  6902  isfi  6933  enssdom  6934  map1  6986  xpcomco  7009  exmidpw  7099  exmidpweq  7100  tpfidceq  7121  fnfi  7134  fidcenumlemrks  7151  fidcenumlemrk  7152  djulclb  7253  eldju  7266  eldju2ndl  7270  eldju2ndr  7271  ctssdccl  7309  pw1nel3  7448  sucpw1nel3  7450  elni  7527  nlt1pig  7560  0nnq  7583  dfmq0qs  7648  dfplq0qs  7649  nqnq0  7660  elinp  7693  0npr  7702  ltdfpr  7725  nqprl  7770  nqpru  7771  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemfl  7794  mulnqprlemfu  7795  cauappcvgprlemladdru  7875  suplocexprlemell  7932  addsrpr  7964  mulsrpr  7965  opelcn  8045  opelreal  8046  elreal  8047  elreal2  8049  0ncn  8050  addcnsr  8053  mulcnsr  8054  addvalex  8063  peano1nnnn  8071  peano2nnnn  8072  xrlenlt  8243  1nn  9153  peano2nn  9154  elnn0  9403  elnnne0  9415  un0addcl  9434  un0mulcl  9435  elxnn0  9466  uztrn2  9773  elnnuz  9792  elnn0uz  9793  elq  9855  elxr  10010  elfzm1b  10332  fz01or  10345  infssuzex  10492  frecfzennn  10687  inftonninf  10703  seqf  10725  ser0  10794  ser0f  10795  hashinfom  11039  iswrd  11114  pfxccatpfx1  11316  clim2ser  11897  clim2ser2  11898  isermulc2  11900  iserle  11902  climserle  11905  fsum3cvg3  11956  isumclim3  11983  isumadd  11991  sumsplitdc  11992  iserabs  12035  cvgcmpub  12036  isumshft  12050  isumsplit  12051  isumlessdc  12056  cvgratz  12092  cvgratgt0  12093  clim2prod  12099  clim2divap  12100  prodf1  12102  zproddc  12139  prodsnf  12152  divides  12349  dvdsflip  12411  nninfctlemfo  12610  ialgrlemconst  12614  prm23lt5  12835  4sqlem2  12961  4sqlem12  12974  ennnfonelemjn  13022  ennnfonelem1  13027  ennnfonelemdm  13040  basmex  13141  ghmeqker  13857  isrhm  14171  rrgmex  14274  lssmex  14368  lidlmex  14488  2idlmex  14514  df2idl2  14522  2idlss  14527  psrbagf  14683  istps  14755  lmss  14969  txuni2  14979  dvply1  15488  sinq34lt0t  15554  lgsdir2lem2  15757  gausslemma2dlem1a  15786  lgsquadlem1  15805  lgsquadlem2  15806  2sqlem1  15842  isuhgrm  15921  isushgrm  15922  isupgren  15945  isumgren  15955  umgredg  15995  umgrpredgv  15997  umgredgne  16000  umgredgnlp  16002  isuspgren  16007  isusgren  16008  ausgrusgrien  16021  usgredgppren  16047  edgssv2en  16049  uspgredg2vlem  16070  uspgredg2v  16071  ushgredgedg  16076  ushgredgedgloop  16078  griedg0ssusgr  16101  uhgrissubgr  16111  subumgredg2en  16121  uhgrspansubgrlem  16126  vtxedgfi  16139  vtxlpfi  16140  vtxdg0v  16144  wlk1walkdom  16209  clwwlkccatlem  16250  clwwlknnn  16262  clwwlknon2x  16285  bdceq  16437  bj-nntrans  16546  bj-nnelirr  16548  ss1oel2o  16586  trilpolemisumle  16642