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