Theorem eqeltri 2213

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltr.1	⊢ 𝐴 = 𝐵
eqeltr.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 ⊢ 𝐵 ∈ 𝐶
2		eqeltr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	eleq1i 2206	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 145	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1332   ∈ wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  eqeltrri  2214  3eltr4i  2222  intab  3808  inex2  4071  vpwex  4111  ord3ex  4122  uniopel  4186  onsucelsucexmid  4453  nnpredcl  4544  elvvuni  4611  isarep2  5218  acexmidlemcase  5777  abrexex2  6030  oprabex  6034  oprabrexex2  6036  rdg0  6292  frecex  6299  1on  6328  2on  6330  3on  6332  4on  6333  1onn  6424  2onn  6425  3onn  6426  4onn  6427  mapsnf1o2  6598  exmidpw  6810  unfiexmid  6814  xpfi  6826  ssfirab  6830  fnfi  6833  iunfidisj  6842  fidcenumlemr  6851  sbthlemi10  6862  ctmlemr  7001  exmidonfinlem  7066  acfun  7080  exmidaclem  7081  ccfunen  7096  nqex  7195  nq0ex  7272  1pr  7386  ltexprlempr  7440  recexprlempr  7464  cauappcvgprlemcl  7485  caucvgprlemcl  7508  caucvgprprlemcl  7536  addvalex  7676  peano1nnnn  7684  peano2nnnn  7685  axcnex  7691  ax1cn  7693  ax1re  7694  pnfxr  7842  mnfxr  7846  inelr  8370  cju  8743  2re  8814  3re  8818  4re  8821  5re  8823  6re  8825  7re  8827  8re  8829  9re  8831  2nn  8905  3nn  8906  4nn  8907  5nn  8908  6nn  8909  7nn  8910  8nn  8911  9nn  8912  nn0ex  9007  nneoor  9177  zeo  9180  deccl  9220  decnncl  9225  numnncl2  9228  decnncl2  9229  numsucc  9245  numma2c  9251  numadd  9252  numaddc  9253  nummul1c  9254  nummul2c  9255  xnegcl  9645  xrex  9669  ioof  9784  uzennn  10240  seqex  10251  m1expcl2  10346  faccl  10513  facwordi  10518  faclbnd2  10520  bccl  10545  crre  10661  remim  10664  absval  10805  climle  11135  climcvg1nlem  11150  iserabs  11276  geo2lim  11317  prodfclim1  11345  ere  11413  ege2le3  11414  eftlub  11433  efsep  11434  tan0  11474  ef01bndlem  11499  nn0o  11640  ennnfonelemj0  11950  ennnfonelem0  11954  ndxarg  12021  ndxslid  12023  strndxid  12026  basendxnn  12053  strle1g  12088  2strbasg  12099  2stropg  12100  setsmsbasg  12687  cnbl0  12742  cnopncntop  12745  remet  12748  divcnap  12763  climcncf  12779  expcncf  12800  cnrehmeocntop  12801  sincn  12898  coscn  12899  2logb9irrALT  13099  2irrexpq  13101  2irrexpqap  13103  bdinex2  13269  bj-inex  13276  012of  13363  2o01f  13364  peano3nninf  13376  nninfex  13380  cvgcmp2nlemabs  13402  trilpolemisumle  13406