Theorem eqeltrd 1163

Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-02.)

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrd

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 |- (ph -> B e. C)
2		eqeltrd.1	. . 3 |- (ph -> A = B)
3	2	eleq1d 1155	. 2 |- (ph -> (A e. C <-> B e. C))
4	1, 3	mpbird 171	1 |- (ph -> A e. C)

Syntax hints:   -> wi 2   = wceq 1091   e. wcel 1092

This theorem is referenced by:  eqeltrrd 1164  onuninsuc 2356  tz9.12lem3 3505  rankon 3515  oncardon 3627  oncardid 3628  cardcf 3706  addclpi 3814  mulclpi 3815  addclpq 3852  mulclpq 3854  addclsr 3986  mulclsr 3987  axaddcl 4066  axaddrcl 4067  axmulcl 4068  axmulrcl 4069  resubclt 4173  nn0addclt 4551  nn0mulcl 4553  zsubclt 4591  flclt 4624  qsubclt 4645  qdivclt 4647  sqclt 4684  reclt 4796  imclt 4797  cjclt 4800  facclt 4874  ruclem13 4897  hvsubclt 4998  normclt 5076  shsubclt 5125  axpjclt 5247  spanclt 5305  hsupclt 5308  sshjclt 5328  spansncht 5465  hosclt 5491  hodclt 5492  spansnsclt 5541  3oalem2 5553  pjocin 5583  hococl 5599  pjcocl 5629  pjcohocl 5655  pj2cocl 5657  mdsymlem1 5776  mdsymlem3 5778

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org