# 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 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 xpexg ${⊢}\left({B}\in {W}\wedge {C}\in {X}\right)\to {B}×{C}\in \mathrm{V}$
2 inxpex ${⊢}\left({R}⋉{S}\in \mathrm{V}\vee \left({A}\in {V}\wedge {B}×{C}\in \mathrm{V}\right)\right)\to {R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\in \mathrm{V}$
3 2 olcs ${⊢}\left({A}\in {V}\wedge {B}×{C}\in \mathrm{V}\right)\to {R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\in \mathrm{V}$
4 1 3 sylan2 ${⊢}\left({A}\in {V}\wedge \left({B}\in {W}\wedge {C}\in {X}\right)\right)\to {R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\in \mathrm{V}$
5 4 3impb ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\in \mathrm{V}$