Metamath Proof Explorer

Theorem inxpex

Description: Sufficient condition for an intersection with a Cartesian product to be a set. (Contributed by Peter Mazsa, 10-May-2019)

Ref Expression
Assertion inxpex 
|- ( ( R e. W \/ ( A e. U /\ B e. V ) ) -> ( R i^i ( A X. B ) ) e. _V )

Proof

Step Hyp Ref Expression
1 inex1g 
 |-  ( R e. W -> ( R i^i ( A X. B ) ) e. _V )
2 xpexg 
 |-  ( ( A e. U /\ B e. V ) -> ( A X. B ) e. _V )
3 inex2g 
 |-  ( ( A X. B ) e. _V -> ( R i^i ( A X. B ) ) e. _V )
4 2 3 syl 
 |-  ( ( A e. U /\ B e. V ) -> ( R i^i ( A X. B ) ) e. _V )
5 1 4 jaoi 
 |-  ( ( R e. W \/ ( A e. U /\ B e. V ) ) -> ( R i^i ( A X. B ) ) e. _V )