Metamath Proof Explorer


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 ) )