Theorem eqeltri 2110

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

Hypotheses

Ref	Expression
eqeltr.1	|- A = B
eqeltr.2	|- B e. C

Assertion

Ref	Expression
eqeltri	|- A e. C

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 |- B e. C
2		eqeltr.1	. . 3 |- A = B
3	2	eleq1i 2103	. 2 |- ( A e. C <-> B e. C )
4	1, 3	mpbir 134	1 |- A e. C

Syntax hints:   = wceq 1243   e. 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:  eqeltrri  2111  3eltr4i  2119  intab  3644  inex2  3892  pwex  3932  ord3ex  3941  uniopel  3993  onsucelsucexmid  4255  elvvuni  4404  isarep2  4986  acexmidlemcase  5507  abrexex2  5751  oprabex  5755  oprabrexex2  5757  rdg0  5974  frecex  5981  1on  6008  2on  6009  3on  6011  4on  6012  1onn  6093  2onn  6094  3onn  6095  4onn  6096  nqex  6461  nq0ex  6538  1pr  6652  ltexprlempr  6706  recexprlempr  6730  cauappcvgprlemcl  6751  caucvgprlemcl  6774  caucvgprprlemcl  6802  addvalex  6920  peano1nnnn  6928  peano2nnnn  6929  axcnex  6935  ax1cn  6937  ax1re  6938  inelr  7575  cju  7913  2re  7985  3re  7989  4re  7992  5re  7994  6re  7996  7re  7998  8re  8000  9re  8002  10re  8004  2nn  8077  3nn  8078  4nn  8079  5nn  8080  6nn  8081  7nn  8082  8nn  8083  9nn  8084  10nn  8085  nn0ex  8187  nneoor  8340  zeo  8343  decnncl  8380  deccl  8381  numnncl2  8384  decnncl2  8385  numsucc  8393  numma2c  8400  numadd  8401  numaddc  8402  nummul1c  8403  nummul2c  8404  pnfxr  8692  mnfxr  8694  xnegcl  8745  xrex  8756  ioof  8840  iseqex  9213  m1expcl2  9277  crre  9457  remim  9460  absval  9599  climle  9854  climcvg1nlem  9868  bdinex2  10020  bj-inex  10027