0nelopab

Description: The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017) Reduce axiom usage and shorten proof. (Revised by GG, 3-Oct-2024)

		Ref	Expression
	Assertion	0nelopab	$⊢ \neg \emptyset \in \{⟨x, y⟩ \| φ\}$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	opnzi	$⊢ ⟨x, y⟩ \neq \emptyset$
4	3	nesymi	$⊢ \neg \emptyset = ⟨x, y⟩$
5	4	intnanr	$⊢ \neg (\emptyset = ⟨x, y⟩ \land φ)$
6	5	nex	$⊢ \neg \exists y (\emptyset = ⟨x, y⟩ \land φ)$
7	6	nex	$⊢ \neg \exists x \exists y (\emptyset = ⟨x, y⟩ \land φ)$
8		elopab	$⊢ \emptyset \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (\emptyset = ⟨x, y⟩ \land φ)$
9	7 8	mtbir	$⊢ \neg \emptyset \in \{⟨x, y⟩ \| φ\}$

Metamath Proof Explorer

Theorem 0nelopab

Proof