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	$$⊢\left(R\in W\vee \left(A\in U\wedge B\in V\right)\right)\to R\cap \left(A\times B\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		inex1g	$$⊢R\in W\to R\cap \left(A\times B\right)\in \mathrm{V}$$
2		xpexg	$$⊢\left(A\in U\wedge B\in V\right)\to A\times B\in \mathrm{V}$$
3		inex2g	$$⊢A\times B\in \mathrm{V}\to R\cap \left(A\times B\right)\in \mathrm{V}$$
4	2 3	syl	$$⊢\left(A\in U\wedge B\in V\right)\to R\cap \left(A\times B\right)\in \mathrm{V}$$
5	1 4	jaoi	$$⊢\left(R\in W\vee \left(A\in U\wedge B\in V\right)\right)\to R\cap \left(A\times B\right)\in \mathrm{V}$$