Theorem eleqtrd 2157

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	|- ( ph -> A e. B )
eleqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eleqtrd	|- ( ph -> A e. C )

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 |- ( ph -> A e. B )
2		eleqtrd.2	. . 3 |- ( ph -> B = C )
3	2	eleq2d 2148	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 145	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = 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:  eleqtrrd  2158  3eltr3d  2161  syl5eleq  2167  syl6eleq  2171  opth1  3991  0nelop  4003  tfisi  4328  ercl  6140  erth  6173  ecelqsdm  6199  phpm  6351  lincmb01cmp  9025  fzopth  9079  fzoaddel2  9202  fzosubel2  9204  fzocatel  9208  zpnn0elfzo1  9217  fzoend  9231  peano2fzor  9241  monoord2  9456  isermono  9457  bcpasc  9693