Theorem eqeltrri

Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypotheses	eqeltrri.1	|- A = B
	eqeltrri.2	|- A e. C
Assertion	eqeltrri	|- B e. C

Proof

Step	Hyp	Ref	Expression
1		eqeltrri.1	|- A = B
2		eqeltrri.2	|- A e. C
3	1	eqcomi	|- B = A
4	3 2	eqeltri	|- B e. C