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 (A \times B) \to \neg \emptyset \in C$

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

Metamath Proof Explorer