Theorem eleq2i 2101

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 2098	. 2 ⊢ (A = B → (𝐶 ∈ A ↔ 𝐶 ∈ B))
3	1, 2	ax-mp 7	1 ⊢ (𝐶 ∈ A ↔ 𝐶 ∈ B)

Syntax hints:   ↔ wb 98   = wceq 1242   ∈ wcel 1390

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033

This theorem is referenced by:  eleq12i  2102  eleqtri  2109  eleq2s  2129  hbxfreq  2141  abeq2i  2145  abeq1i  2146  nfceqi  2171  raleqbii  2330  rexeqbii  2331  rabeq2i  2548  elab2g  2683  elrabf  2690  elrab3t  2691  elrab2  2694  cbvsbc  2785  elin2  3121  dfnul2  3220  noel  3222  rabn0m  3239  rabeq0  3241  eltpg  3407  tpid3g  3474  oprcl  3564  elunirab  3584  elintrab  3618  exss  3954  elop  3959  opm  3962  brabsb  3989  brabga  3992  pofun  4040  elsuci  4106  elsucg  4107  elsuc2g  4108  ordsucim  4192  peano2  4261  elxp  4305  brab2a  4336  brab2ga  4358  elcnv  4455  dmmrnm  4497  elrnmptg  4529  opelres  4560  rninxp  4707  funco  4883  elfv  5119  nfvres  5149  fvopab3g  5188  fvmptssdm  5198  fmptco  5273  funfvima  5333  fliftel  5376  acexmidlema  5446  acexmidlemb  5447  acexmidlem2  5452  eloprabga  5533  elrnmpt2  5556  ovid  5559  offval  5661  xporderlem  5793  brtpos2  5807  issmo  5844  smores3  5849  tfrlem7  5874  tfrlem9  5876  tfr0  5878  tfri2  5893  el1o  5959  dif1o  5960  elecg  6080  brecop  6132  erovlem  6134  oviec  6148  isfi  6177  enssdom  6178  xpcomco  6236  elni  6292  nlt1pig  6325  0nnq  6348  dfmq0qs  6411  dfplq0qs  6412  nqnq0  6423  elinp  6456  0npr  6465  ltdfpr  6488  nqprl  6532  addnqprlemfl  6539  addnqprlemfu  6540  cauappcvgprlemladdru  6627  addsrpr  6653  mulsrpr  6654  opelcn  6705  opelreal  6706  elreal  6707  elreal2  6708  0ncn  6709  addcnsr  6711  mulcnsr  6712  xrlenlt  6861  1nn  7686  peano2nn  7687  elnn0  7939  elnnne0  7951  un0addcl  7971  un0mulcl  7972  uztrn2  8246  elnnuz  8265  elnn0uz  8266  elq  8313  elxr  8446  elfzm1b  8710  frecfzennn  8864  bdceq  9277  bj-nntrans  9385  bj-nnelirr  9387