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  6412  dfplq0qs  6413  nqnq0  6424  elinp  6457  0npr  6466  ltdfpr  6489  nqprl  6533  addnqprlemfl  6540  addnqprlemfu  6541  cauappcvgprlemladdru  6628  addsrpr  6673  mulsrpr  6674  opelcn  6725  opelreal  6726  elreal  6727  elreal2  6728  0ncn  6729  addcnsr  6731  mulcnsr  6732  xrlenlt  6881  1nn  7706  peano2nn  7707  elnn0  7959  elnnne0  7971  un0addcl  7991  un0mulcl  7992  uztrn2  8266  elnnuz  8285  elnn0uz  8286  elq  8333  elxr  8466  elfzm1b  8730  frecfzennn  8884  bdceq  9297  bj-nntrans  9411  bj-nnelirr  9413