Theorem eqeltrrd

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

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

Proof

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