Theorem xp0

Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of Monk1 p. 37. (Contributed by NM, 12-Apr-2004) Avoid axioms. (Revised by TM, 1-Feb-2026)

	Ref	Expression
Assertion	xp0	$$⊢A\times \varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg y\in \varnothing$$
2		simprr	$$⊢\left(z=⟨x,y⟩\wedge \left(x\in A\wedge y\in \varnothing \right)\right)\to y\in \varnothing$$
3	1 2	mto	$$⊢\neg \left(z=⟨x,y⟩\wedge \left(x\in A\wedge y\in \varnothing \right)\right)$$
4	3	nex	$$⊢\neg \exists y\left(z=⟨x,y⟩\wedge \left(x\in A\wedge y\in \varnothing \right)\right)$$
5	4	nex	$$⊢\neg \exists x\exists y\left(z=⟨x,y⟩\wedge \left(x\in A\wedge y\in \varnothing \right)\right)$$
6		elxpi	$$⊢z\in \left(A\times \varnothing \right)\to \exists x\exists y\left(z=⟨x,y⟩\wedge \left(x\in A\wedge y\in \varnothing \right)\right)$$
7	5 6	mto	$$⊢\neg z\in \left(A\times \varnothing \right)$$
8	7	nel0	$$⊢A\times \varnothing =\varnothing$$