Theorem eleq2i 2299

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

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

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

This theorem is referenced by:  eleq12i  2300  eleqtri  2307  eleq2s  2327  hbxfreq  2339  abeq2i  2343  abeq1i  2344  nfceqi  2380  raleqbii  2554  rexeqbii  2555  reqabi  2720  rabeq2i  2810  elab2g  2964  elrabf  2971  elrab3t  2972  elrab2  2976  cbvsbcw  3070  cbvsbc  3071  csbcow  3149  elin2  3407  dfnul2  3510  noel  3512  rabn0m  3536  rabeq0  3538  eltpg  3734  tpid3g  3807  oprcl  3907  elunirab  3927  elintrab  3961  exss  4343  elop  4347  opm  4350  brabsb  4379  brabga  4382  pofun  4433  elsuci  4524  elsucg  4525  elsuc2g  4526  ordsucim  4622  peano2  4717  elxp  4766  brab2a  4803  brab2ga  4825  elco  4921  elcnv  4932  dmmrnm  4976  elrnmptg  5009  opelres  5043  rninxp  5206  eliota  5340  funco  5392  elfv  5668  nfvres  5706  fvopab3g  5750  fvmptssdm  5762  fmptco  5843  funfvima  5918  fliftel  5966  acexmidlema  6041  acexmidlemb  6042  acexmidlem2  6047  eloprabga  6140  elrnmpo  6167  ovid  6170  offval  6274  xporderlem  6427  brtpos2  6482  issmo  6519  smores3  6524  tfrlem7  6548  tfrlem9  6550  tfr0dm  6553  tfri2  6597  rdgon  6617  freccllem  6633  frecfcllem  6635  frecsuclem  6637  el1o  6670  dif1o  6671  nnsucuniel  6728  elecg  6807  brecop  6859  erovlem  6861  oviec  6875  mapsncnv  6930  mptelixpg  6969  isfi  7000  enssdom  7001  map1  7054  xpcomco  7077  exmidpw  7168  exmidpweq  7169  tpfidceq  7190  fnfi  7203  fidcenumlemrks  7223  fidcenumlemrk  7224  djulclb  7346  eldju  7359  eldju2ndl  7363  eldju2ndr  7364  ctssdccl  7402  pw1nel3  7541  sucpw1nel3  7543  elni  7623  nlt1pig  7656  0nnq  7679  dfmq0qs  7744  dfplq0qs  7745  nqnq0  7756  elinp  7789  0npr  7798  ltdfpr  7821  nqprl  7866  nqpru  7867  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemfl  7890  mulnqprlemfu  7891  cauappcvgprlemladdru  7971  suplocexprlemell  8028  addsrpr  8060  mulsrpr  8061  opelcn  8141  opelreal  8142  elreal  8143  elreal2  8145  0ncn  8146  addcnsr  8149  mulcnsr  8150  addvalex  8159  peano1nnnn  8167  peano2nnnn  8168  xrlenlt  8338  1nn  9248  peano2nn  9249  elnn0  9498  elnnne0  9510  un0addcl  9529  un0mulcl  9530  elxnn0  9565  uztrn2  9872  elnnuz  9891  elnn0uz  9892  elq  9954  elxr  10109  elfzm1b  10432  fz01or  10445  infssuzex  10593  frecfzennn  10788  inftonninf  10804  seqf  10826  ser0  10895  ser0f  10896  hashinfom  11141  iswrd  11226  pfxccatpfx1  11428  clim2ser  12022  clim2ser2  12023  isermulc2  12025  iserle  12027  climserle  12030  fsum3cvg3  12082  isumclim3  12109  isumadd  12117  sumsplitdc  12118  iserabs  12161  cvgcmpub  12162  isumshft  12176  isumsplit  12177  isumlessdc  12182  cvgratz  12218  cvgratgt0  12219  clim2prod  12225  clim2divap  12226  prodf1  12228  zproddc  12265  prodsnf  12278  divides  12475  dvdsflip  12537  nninfctlemfo  12736  ialgrlemconst  12740  prm23lt5  12961  4sqlem2  13087  4sqlem12  13100  ennnfonelemjn  13153  ennnfonelem1  13158  ennnfonelemdm  13171  basmex  13272  ghmeqker  13988  isrhm  14303  rrgmex  14406  lssmex  14503  lidlmex  14623  2idlmex  14649  df2idl2  14657  2idlss  14662  psrbagf  14818  istps  14897  lmss  15111  txuni2  15121  dvply1  15630  sinq34lt0t  15696  lgsdir2lem2  15902  gausslemma2dlem1a  15931  lgsquadlem1  15950  lgsquadlem2  15951  2sqlem1  15987  isuhgrm  16066  isushgrm  16067  isupgren  16090  isumgren  16100  umgredg  16140  umgrpredgv  16142  umgredgne  16145  umgredgnlp  16147  isuspgren  16152  isusgren  16153  ausgrusgrien  16166  usgredgppren  16192  edgssv2en  16194  uspgredg2vlem  16215  uspgredg2v  16216  ushgredgedg  16221  ushgredgedgloop  16223  griedg0ssusgr  16246  uhgrissubgr  16256  subumgredg2en  16266  uhgrspansubgrlem  16271  vtxedgfi  16284  vtxlpfi  16285  vtxdg0v  16289  wlk1walkdom  16354  clwwlkccatlem  16395  clwwlknnn  16407  clwwlknon2x  16430  bdceq  16612  bj-nntrans  16721  bj-nnelirr  16723  ss1oel2o  16761  trilpolemisumle  16822