Theorem elrint

Description: Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	elrint	|- ( X e. ( A i^i |^| B ) <-> ( X e. A /\ A. y e. B X e. y ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( X e. ( A i^i |^| B ) <-> ( X e. A /\ X e. |^| B ) )
2		elintg	|- ( X e. A -> ( X e. |^| B <-> A. y e. B X e. y ) )
3	2	pm5.32i	|- ( ( X e. A /\ X e. |^| B ) <-> ( X e. A /\ A. y e. B X e. y ) )
4	1 3	bitri	|- ( X e. ( A i^i |^| B ) <-> ( X e. A /\ A. y e. B X e. y ) )