Theorem elrint2

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

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

Proof

Step	Hyp	Ref	Expression
1		elrint	|- ( X e. ( A i^i |^| B ) <-> ( X e. A /\ A. y e. B X e. y ) )
2	1	baib	|- ( X e. A -> ( X e. ( A i^i |^| B ) <-> A. y e. B X e. y ) )