Theorem eleq2s

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

	Ref	Expression
Hypotheses	eleq2s.1	$$⊢A\in B\to \phi$$
	eleq2s.2	$$⊢C=B$$
Assertion	eleq2s	$$⊢A\in C\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		eleq2s.1	$$⊢A\in B\to \phi$$
2		eleq2s.2	$$⊢C=B$$
3	2	eleq2i	$$⊢A\in C\leftrightarrow A\in B$$
4	3 1	sylbi	$$⊢A\in C\to \phi$$