Theorem eleq2i 2161

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

Syntax hints:   ↔ wb 104   = wceq 1296   ∈ wcel 1445

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091

This theorem is referenced by:  eleq12i  2162  eleqtri  2169  eleq2s  2189  hbxfreq  2201  abeq2i  2205  abeq1i  2206  nfceqi  2231  raleqbii  2401  rexeqbii  2402  rabeq2i  2630  elab2g  2776  elrabf  2783  elrab3t  2784  elrab2  2788  cbvsbc  2881  elin2  3203  dfnul2  3304  noel  3306  rabn0m  3329  rabeq0  3331  eltpg  3508  tpid3g  3577  oprcl  3668  elunirab  3688  elintrab  3722  exss  4078  elop  4082  opm  4085  brabsb  4112  brabga  4115  pofun  4163  elsuci  4254  elsucg  4255  elsuc2g  4256  ordsucim  4345  peano2  4438  elxp  4484  brab2a  4520  brab2ga  4542  elco  4633  elcnv  4644  dmmrnm  4686  elrnmptg  4719  opelres  4750  rninxp  4908  funco  5088  elfv  5338  nfvres  5372  fvopab3g  5412  fvmptssdm  5423  fmptco  5503  funfvima  5565  fliftel  5610  acexmidlema  5681  acexmidlemb  5682  acexmidlem2  5687  eloprabga  5773  elrnmpt2  5796  ovid  5799  offval  5901  xporderlem  6034  brtpos2  6054  issmo  6091  smores3  6096  tfrlem7  6120  tfrlem9  6122  tfr0dm  6125  tfri2  6169  rdgon  6189  freccllem  6205  frecfcllem  6207  frecsuclem  6209  el1o  6239  dif1o  6240  nnsucuniel  6296  elecg  6370  brecop  6422  erovlem  6424  oviec  6438  mapsncnv  6492  mptelixpg  6531  isfi  6558  enssdom  6559  map1  6609  xpcomco  6622  exmidpw  6704  fnfi  6726  fidcenumlemrks  6742  fidcenumlemrk  6743  djulclb  6827  djur  6837  eldju  6839  eldju2ndl  6843  eldju2ndr  6844  elni  6964  nlt1pig  6997  0nnq  7020  dfmq0qs  7085  dfplq0qs  7086  nqnq0  7097  elinp  7130  0npr  7139  ltdfpr  7162  nqprl  7207  nqpru  7208  addnqprlemfl  7215  addnqprlemfu  7216  mulnqprlemfl  7231  mulnqprlemfu  7232  cauappcvgprlemladdru  7312  addsrpr  7388  mulsrpr  7389  opelcn  7461  opelreal  7462  elreal  7463  elreal2  7465  0ncn  7466  addcnsr  7468  mulcnsr  7469  addvalex  7478  peano1nnnn  7486  peano2nnnn  7487  xrlenlt  7648  1nn  8531  peano2nn  8532  elnn0  8773  elnnne0  8785  un0addcl  8804  un0mulcl  8805  elxnn0  8836  uztrn2  9135  elnnuz  9154  elnn0uz  9155  elq  9206  elxr  9346  elfzm1b  9661  fz01or  9674  frecfzennn  9982  inftonninf  9996  iseqfcl  10024  iseqfclt  10025  seqf  10026  ser0  10080  ser0f  10081  hashinfom  10317  clim2ser  10895  clim2ser2  10896  isermulc2  10898  iserle  10900  climserle  10903  fsum3cvg3  10954  isumclim3  10981  isumadd  10989  sumsplitdc  10990  iserabs  11033  cvgcmpub  11034  isumshft  11048  isumsplit  11049  isumlessdc  11054  cvgratz  11090  cvgratgt0  11091  divides  11240  dvdsflip  11294  infssuzex  11387  ialgrlemconst  11467  istps  11897  lmss  12112  bdceq  12445  bj-nntrans  12558  bj-nnelirr  12560  ss1oel2o  12598