Theorem eqeltri 2151

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 2144	. 2 |- ( A e. C <-> B e. C )
4	1, 3	mpbir 144	1 |- A e. C

Syntax hints:   = wceq 1284   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  eqeltrri  2152  3eltr4i  2160  intab  3665  inex2  3913  pwex  3953  ord3ex  3961  uniopel  4011  onsucelsucexmid  4273  elvvuni  4422  isarep2  5006  acexmidlemcase  5527  abrexex2  5771  oprabex  5775  oprabrexex2  5777  rdg0  5997  frecex  6004  1on  6031  2on  6032  3on  6034  4on  6035  1onn  6116  2onn  6117  3onn  6118  4onn  6119  fnfi  6388  nqex  6553  nq0ex  6630  1pr  6744  ltexprlempr  6798  recexprlempr  6822  cauappcvgprlemcl  6843  caucvgprlemcl  6866  caucvgprprlemcl  6894  addvalex  7012  peano1nnnn  7020  peano2nnnn  7021  axcnex  7027  ax1cn  7029  ax1re  7030  inelr  7684  cju  8038  2re  8109  3re  8113  4re  8116  5re  8118  6re  8120  7re  8122  8re  8124  9re  8126  2nn  8193  3nn  8194  4nn  8195  5nn  8196  6nn  8197  7nn  8198  8nn  8199  9nn  8200  nn0ex  8294  nneoor  8449  zeo  8452  deccl  8491  decnncl  8496  numnncl2  8499  decnncl2  8500  numsucc  8516  numma2c  8522  numadd  8523  numaddc  8524  nummul1c  8525  nummul2c  8526  pnfxr  8846  mnfxr  8848  xnegcl  8899  xrex  8910  ioof  8994  iseqex  9433  m1expcl2  9498  faccl  9662  facwordi  9667  faclbnd2  9669  bccl  9694  crre  9744  remim  9747  absval  9887  climle  10172  climcvg1nlem  10186  nn0o  10307  bdinex2  10691  bj-inex  10698