Metamath Proof Explorer


Theorem xrninxpex

Description: Sufficient condition for the intersection of a range Cartesian product with a Cartesian product to be a set. (Contributed by Peter Mazsa, 12-Apr-2020)

Ref Expression
Assertion xrninxpex AVBWCXRSA×B×CV

Proof

Step Hyp Ref Expression
1 xpexg BWCXB×CV
2 inxpex RSVAVB×CVRSA×B×CV
3 2 olcs AVB×CVRSA×B×CV
4 1 3 sylan2 AVBWCXRSA×B×CV
5 4 3impb AVBWCXRSA×B×CV