Theorem eqeltri

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

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

Proof

Step	Hyp	Ref	Expression
1		eqeltri.1	⊢ 𝐴 = 𝐵
2		eqeltri.2	⊢ 𝐵 ∈ 𝐶
3	1	eleq1i	⊢ ( 𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 )
4	2 3	mpbir	⊢ 𝐴 ∈ 𝐶