Theorem eqeltrri

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

	Ref	Expression
Hypotheses	eqeltrri.1	⊢ 𝐴 = 𝐵
	eqeltrri.2	⊢ 𝐴 ∈ 𝐶
Assertion	eqeltrri	⊢ 𝐵 ∈ 𝐶

Proof

Step	Hyp	Ref	Expression
1		eqeltrri.1	⊢ 𝐴 = 𝐵
2		eqeltrri.2	⊢ 𝐴 ∈ 𝐶
3	1	eqcomi	⊢ 𝐵 = 𝐴
4	3 2	eqeltri	⊢ 𝐵 ∈ 𝐶