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  3406  tpid3g  3473  oprcl  3563  elunirab  3583  elintrab  3617  exss  3953  elop  3958  opm  3961  brabsb  3988  brabga  3991  pofun  4039  elsuci  4105  elsucg  4106  elsuc2g  4107  ordsucim  4191  peano2  4260  elxp  4304  brab2a  4335  brab2ga  4357  elcnv  4454  dmmrnm  4496  elrnmptg  4528  opelres  4559  rninxp  4706  funco  4881  elfv  5117  nfvres  5147  fvopab3g  5186  fvmptssdm  5196  fmptco  5271  funfvima  5331  fliftel  5374  acexmidlema  5443  acexmidlemb  5444  acexmidlem2  5449  eloprabga  5530  elrnmpt2  5553  ovid  5556  offval  5658  xporderlem  5790  brtpos2  5804  issmo  5841  smores3  5846  tfrlem7  5871  tfrlem9  5873  tfr0  5875  tfri2  5890  el1o  5952  dif1o  5953  elecg  6073  brecop  6125  erovlem  6127  oviec  6141  isfi  6170  enssdom  6171  xpcomco  6229  elni  6285  nlt1pig  6318  0nnq  6341  dfmq0qs  6404  dfplq0qs  6405  nqnq0  6416  elinp  6449  0npr  6458  ltdfpr  6481  addnqpr1lemil  6531  addnqpr1lemiu  6532  addsrpr  6625  mulsrpr  6626  opelcn  6677  opelreal  6678  elreal  6679  elreal2  6680  0ncn  6681  addcnsr  6683  mulcnsr  6684  xrlenlt  6833  1nn  7657  peano2nn  7658  elnn0  7909  elnnne0  7921  un0addcl  7941  un0mulcl  7942  uztrn2  8215  elnnuz  8234  elnn0uz  8235  elq  8282  elxr  8414  elfzm1b  8676  frecfzennn  8822  bdceq  8896  bj-nntrans  9004  bj-nnelirr  9006