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\in C$$
Assertion	eqeltrri	$$⊢B\in C$$

Proof

Step	Hyp	Ref	Expression
1		eqeltrri.1	$$⊢A=B$$
2		eqeltrri.2	$$⊢A\in C$$
3	1	eqcomi	$$⊢B=A$$
4	3 2	eqeltri	$$⊢B\in C$$