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 e. B -> ph )
	eleq2s.2	|- C = B
Assertion	eleq2s	|- ( A e. C -> ph )

Proof

Step	Hyp	Ref	Expression
1		eleq2s.1	|- ( A e. B -> ph )
2		eleq2s.2	|- C = B
3	2	eleq2i	|- ( A e. C <-> A e. B )
4	3 1	sylbi	|- ( A e. C -> ph )