Theorem elind

Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	elind.1	|- ( ph -> X e. A )
	elind.2	|- ( ph -> X e. B )
Assertion	elind	|- ( ph -> X e. ( A i^i B ) )

Proof

Step	Hyp	Ref	Expression
1		elind.1	|- ( ph -> X e. A )
2		elind.2	|- ( ph -> X e. B )
3		elin	|- ( X e. ( A i^i B ) <-> ( X e. A /\ X e. B ) )
4	1 2 3	sylanbrc	|- ( ph -> X e. ( A i^i B ) )