Theorem xpeq0

Description: At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006)

	Ref	Expression
Assertion	xpeq0	$$⊢A\times B=\varnothing \leftrightarrow \left(A=\varnothing \vee B=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		xpnz	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow A\times B\ne \varnothing$$
2	1	necon2bbii	$$⊢A\times B=\varnothing \leftrightarrow \neg \left(A\ne \varnothing \wedge B\ne \varnothing \right)$$
3		ianor	$$⊢\neg \left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow \left(\neg A\ne \varnothing \vee \neg B\ne \varnothing \right)$$
4		nne	$$⊢\neg A\ne \varnothing \leftrightarrow A=\varnothing$$
5		nne	$$⊢\neg B\ne \varnothing \leftrightarrow B=\varnothing$$
6	4 5	orbi12i	$$⊢\left(\neg A\ne \varnothing \vee \neg B\ne \varnothing \right)\leftrightarrow \left(A=\varnothing \vee B=\varnothing \right)$$
7	2 3 6	3bitri	$$⊢A\times B=\varnothing \leftrightarrow \left(A=\varnothing \vee B=\varnothing \right)$$