Theorem eleq2i 2104

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

Syntax hints:   ↔ wb 98   = wceq 1243   ∈ wcel 1393

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

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

This theorem is referenced by:  eleq12i  2105  eleqtri  2112  eleq2s  2132  hbxfreq  2144  abeq2i  2148  abeq1i  2149  nfceqi  2174  raleqbii  2336  rexeqbii  2337  rabeq2i  2554  elab2g  2689  elrabf  2696  elrab3t  2697  elrab2  2700  cbvsbc  2791  elin2  3127  dfnul2  3226  noel  3228  rabn0m  3245  rabeq0  3247  eltpg  3416  tpid3g  3483  oprcl  3573  elunirab  3593  elintrab  3627  exss  3963  elop  3968  opm  3971  brabsb  3998  brabga  4001  pofun  4049  elsuci  4140  elsucg  4141  elsuc2g  4142  ordsucim  4226  peano2  4318  elxp  4362  brab2a  4393  brab2ga  4415  elcnv  4512  dmmrnm  4554  elrnmptg  4586  opelres  4617  rninxp  4764  funco  4940  elfv  5176  nfvres  5206  fvopab3g  5245  fvmptssdm  5255  fmptco  5330  funfvima  5390  fliftel  5433  acexmidlema  5503  acexmidlemb  5504  acexmidlem2  5509  eloprabga  5591  elrnmpt2  5614  ovid  5617  offval  5719  xporderlem  5852  brtpos2  5866  issmo  5903  smores3  5908  tfrlem7  5933  tfrlem9  5935  tfr0  5937  tfri2  5952  el1o  6020  dif1o  6021  elecg  6144  brecop  6196  erovlem  6198  oviec  6212  isfi  6241  enssdom  6242  xpcomco  6300  elni  6406  nlt1pig  6439  0nnq  6462  dfmq0qs  6527  dfplq0qs  6528  nqnq0  6539  elinp  6572  0npr  6581  ltdfpr  6604  nqprl  6649  nqpru  6650  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemfl  6673  mulnqprlemfu  6674  cauappcvgprlemladdru  6754  addsrpr  6830  mulsrpr  6831  opelcn  6903  opelreal  6904  elreal  6905  elreal2  6907  0ncn  6908  addcnsr  6910  mulcnsr  6911  addvalex  6920  peano1nnnn  6928  peano2nnnn  6929  xrlenlt  7084  1nn  7925  peano2nn  7926  elnn0  8183  elnnne0  8195  un0addcl  8215  un0mulcl  8216  uztrn2  8490  elnnuz  8509  elnn0uz  8510  elq  8557  elxr  8696  elfzm1b  8960  frecfzennn  9203  iseqf  9224  iser0  9250  iser0f  9251  clim2iser  9857  clim2iser2  9858  iisermulc2  9860  iserile  9862  climserile  9865  ialgrlemconst  9882  ialgrf  9884  bdceq  9962  bj-nntrans  10076  bj-nnelirr  10078