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 RWAUBVRA×BV

Proof

Step Hyp Ref Expression
1 inex1g RWRA×BV
2 xpexg AUBVA×BV
3 inex2g A×BVRA×BV
4 2 3 syl AUBVRA×BV
5 1 4 jaoi RWAUBVRA×BV