Theorem eleq2i 2082

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

Hypothesis

Ref	Expression
eleq1i.1	⊢ A = B

Assertion

Ref	Expression
eleq2i	⊢ (𝐶 ∈ A ↔ 𝐶 ∈ B)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ A = B
2		eleq2 2079	. 2 ⊢ (A = B → (𝐶 ∈ A ↔ 𝐶 ∈ B))
3	1, 2	ax-mp 7	1 ⊢ (𝐶 ∈ A ↔ 𝐶 ∈ B)

Syntax hints:   ↔ wb 98   = wceq 1226   ∈ wcel 1370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-cleq 2011  df-clel 2014

This theorem is referenced by:  eleq12i  2083  eleqtri  2090  eleq2s  2110  hbxfreq  2122  abeq2i  2126  abeq1i  2127  nfceqi  2152  raleqbii  2310  rexeqbii  2311  rabeq2i  2528  elab2g  2662  elrabf  2669  elrab3t  2670  elrab2  2673  cbvsbc  2764  elin2  3100  dfnul2  3199  noel  3201  rabn0m  3218  rabeq0  3220  eltpg  3386  tpid3g  3453  oprcl  3543  elunirab  3563  elintrab  3597  exss  3933  elop  3938  opm  3941  brabsb  3968  brabga  3971  pofun  4019  elsuci  4085  elsucg  4086  elsuc2g  4087  ordsucim  4172  peano2  4241  elxp  4285  brab2a  4316  brab2ga  4338  elcnv  4435  dmmrnm  4477  elrnmptg  4509  opelres  4540  rninxp  4687  funco  4862  elfv  5097  nfvres  5127  fvopab3g  5166  fvmptssdm  5176  fmptco  5251  funfvima  5311  fliftel  5354  acexmidlema  5423  acexmidlemb  5424  acexmidlem2  5429  eloprabga  5510  elrnmpt2  5533  ovid  5536  offval  5638  xporderlem  5770  brtpos2  5784  issmo  5821  smores3  5826  tfrlem7  5851  tfrlem9  5853  tfri2  5870  el1o  5931  dif1o  5932  elecg  6051  brecop  6103  erovlem  6105  oviec  6119  elni  6162  nlt1pig  6195  0nnq  6217  dfmq0qs  6278  dfplq0qs  6279  nqnq0  6290  elinp  6322  0npr  6331  ltdfpr  6354  addsrpr  6486  mulsrpr  6487  opelcn  6533  opelreal  6534  elreal  6535  elreal2  6536  0ncn  6537  addcnsr  6539  mulcnsr  6540  xrlenlt  6679  bdceq  7208  bj-nntrans  7312  bj-nnelirr  7314