Theorem eqeltrd

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

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

Proof

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