Theorem eleq2i 2296

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

Syntax hints:   ↔ wb 105   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12i  2297  eleqtri  2304  eleq2s  2324  hbxfreq  2336  abeq2i  2340  abeq1i  2341  nfceqi  2368  raleqbii  2542  rexeqbii  2543  rabeq2i  2796  elab2g  2950  elrabf  2957  elrab3t  2958  elrab2  2962  cbvsbcw  3056  cbvsbc  3057  csbcow  3135  elin2  3392  dfnul2  3493  noel  3495  rabn0m  3519  rabeq0  3521  eltpg  3711  tpid3g  3782  oprcl  3881  elunirab  3901  elintrab  3935  exss  4313  elop  4317  opm  4320  brabsb  4349  brabga  4352  pofun  4403  elsuci  4494  elsucg  4495  elsuc2g  4496  ordsucim  4592  peano2  4687  elxp  4736  brab2a  4772  brab2ga  4794  elco  4888  elcnv  4899  dmmrnm  4943  elrnmptg  4976  opelres  5010  rninxp  5172  eliota  5306  funco  5358  elfv  5627  nfvres  5665  fvopab3g  5709  fvmptssdm  5721  fmptco  5803  funfvima  5875  fliftel  5923  acexmidlema  5998  acexmidlemb  5999  acexmidlem2  6004  eloprabga  6097  elrnmpo  6124  ovid  6127  offval  6232  xporderlem  6383  brtpos2  6403  issmo  6440  smores3  6445  tfrlem7  6469  tfrlem9  6471  tfr0dm  6474  tfri2  6518  rdgon  6538  freccllem  6554  frecfcllem  6556  frecsuclem  6558  el1o  6591  dif1o  6592  nnsucuniel  6649  elecg  6728  brecop  6780  erovlem  6782  oviec  6796  mapsncnv  6850  mptelixpg  6889  isfi  6920  enssdom  6921  map1  6973  xpcomco  6993  exmidpw  7081  exmidpweq  7082  tpfidceq  7103  fnfi  7114  fidcenumlemrks  7131  fidcenumlemrk  7132  djulclb  7233  eldju  7246  eldju2ndl  7250  eldju2ndr  7251  ctssdccl  7289  pw1nel3  7427  sucpw1nel3  7429  elni  7506  nlt1pig  7539  0nnq  7562  dfmq0qs  7627  dfplq0qs  7628  nqnq0  7639  elinp  7672  0npr  7681  ltdfpr  7704  nqprl  7749  nqpru  7750  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  cauappcvgprlemladdru  7854  suplocexprlemell  7911  addsrpr  7943  mulsrpr  7944  opelcn  8024  opelreal  8025  elreal  8026  elreal2  8028  0ncn  8029  addcnsr  8032  mulcnsr  8033  addvalex  8042  peano1nnnn  8050  peano2nnnn  8051  xrlenlt  8222  1nn  9132  peano2nn  9133  elnn0  9382  elnnne0  9394  un0addcl  9413  un0mulcl  9414  elxnn0  9445  uztrn2  9752  elnnuz  9771  elnn0uz  9772  elq  9829  elxr  9984  elfzm1b  10306  fz01or  10319  infssuzex  10465  frecfzennn  10660  inftonninf  10676  seqf  10698  ser0  10767  ser0f  10768  hashinfom  11012  iswrd  11086  pfxccatpfx1  11283  clim2ser  11863  clim2ser2  11864  isermulc2  11866  iserle  11868  climserle  11871  fsum3cvg3  11922  isumclim3  11949  isumadd  11957  sumsplitdc  11958  iserabs  12001  cvgcmpub  12002  isumshft  12016  isumsplit  12017  isumlessdc  12022  cvgratz  12058  cvgratgt0  12059  clim2prod  12065  clim2divap  12066  prodf1  12068  zproddc  12105  prodsnf  12118  divides  12315  dvdsflip  12377  nninfctlemfo  12576  ialgrlemconst  12580  prm23lt5  12801  4sqlem2  12927  4sqlem12  12940  ennnfonelemjn  12988  ennnfonelem1  12993  ennnfonelemdm  13006  basmex  13107  ghmeqker  13823  isrhm  14137  rrgmex  14240  lssmex  14334  lidlmex  14454  2idlmex  14480  df2idl2  14488  2idlss  14493  psrbagf  14649  istps  14721  lmss  14935  txuni2  14945  dvply1  15454  sinq34lt0t  15520  lgsdir2lem2  15723  gausslemma2dlem1a  15752  lgsquadlem1  15771  lgsquadlem2  15772  2sqlem1  15808  isuhgrm  15886  isushgrm  15887  isupgren  15910  isumgren  15920  umgredg  15958  umgrpredgv  15960  umgredgne  15963  umgredgnlp  15965  isuspgren  15970  isusgren  15971  ausgrusgrien  15984  usgredgppren  16010  edgssv2en  16012  uspgredg2vlem  16033  uspgredg2v  16034  ushgredgedg  16039  ushgredgedgloop  16041  vtxedgfi  16048  vtxlpfi  16049  vtxdg0v  16053  wlk1walkdom  16100  clwwlkccatlem  16137  bdceq  16260  bj-nntrans  16369  bj-nnelirr  16371  ss1oel2o  16410  trilpolemisumle  16466