Metamath Proof Explorer


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