Theorem 0nelelxp

Description: A member of a Cartesian product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008)

	Ref	Expression
Assertion	0nelelxp	$$⊢C\in \left(A\times B\right)\to \neg \varnothing \in C$$

Proof

Step	Hyp	Ref	Expression
1		elxp	$$⊢C\in \left(A\times B\right)\leftrightarrow \exists x\exists y\left(C=⟨x,y⟩\wedge \left(x\in A\wedge y\in B\right)\right)$$
2		0nelop	$$⊢\neg \varnothing \in ⟨x,y⟩$$
3		eleq2	$$⊢C=⟨x,y⟩\to \left(\varnothing \in C\leftrightarrow \varnothing \in ⟨x,y⟩\right)$$
4	2 3	mtbiri	$$⊢C=⟨x,y⟩\to \neg \varnothing \in C$$
5	4	adantr	$$⊢\left(C=⟨x,y⟩\wedge \left(x\in A\wedge y\in B\right)\right)\to \neg \varnothing \in C$$
6	5	exlimivv	$$⊢\exists x\exists y\left(C=⟨x,y⟩\wedge \left(x\in A\wedge y\in B\right)\right)\to \neg \varnothing \in C$$
7	1 6	sylbi	$$⊢C\in \left(A\times B\right)\to \neg \varnothing \in C$$