Theorem eleq2s

Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	eleq2s.1	⊢ ( 𝐴 ∈ 𝐵 → 𝜑 )
	eleq2s.2	⊢ 𝐶 = 𝐵
Assertion	eleq2s	⊢ ( 𝐴 ∈ 𝐶 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		eleq2s.1	⊢ ( 𝐴 ∈ 𝐵 → 𝜑 )
2		eleq2s.2	⊢ 𝐶 = 𝐵
3	2	eleq2i	⊢ ( 𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵 )
4	3 1	sylbi	⊢ ( 𝐴 ∈ 𝐶 → 𝜑 )