opabn0

Description: Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007)

		Ref	Expression
	Assertion	opabn0	$⊢ \{⟨x, y⟩ \| φ\} \neq \emptyset \leftrightarrow \exists x \exists y φ$

Step	Hyp	Ref	Expression
1		n0	$⊢ \{⟨x, y⟩ \| φ\} \neq \emptyset \leftrightarrow \exists z z \in \{⟨x, y⟩ \| φ\}$
2		elopab	$⊢ z \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land φ)$
3	2	exbii	$⊢ \exists z z \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists z \exists x \exists y (z = ⟨x, y⟩ \land φ)$
4		exrot3	$⊢ \exists z \exists x \exists y (z = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (z = ⟨x, y⟩ \land φ)$
5		opex	$⊢ ⟨x, y⟩ \in V$
6	5	isseti	$⊢ \exists z z = ⟨x, y⟩$
7		19.41v	$⊢ \exists z (z = ⟨x, y⟩ \land φ) \leftrightarrow (\exists z z = ⟨x, y⟩ \land φ)$
8	6 7	mpbiran	$⊢ \exists z (z = ⟨x, y⟩ \land φ) \leftrightarrow φ$
9	8	2exbii	$⊢ \exists x \exists y \exists z (z = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y φ$
10	4 9	bitri	$⊢ \exists z \exists x \exists y (z = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y φ$
11	3 10	bitri	$⊢ \exists z z \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y φ$
12	1 11	bitri	$⊢ \{⟨x, y⟩ \| φ\} \neq \emptyset \leftrightarrow \exists x \exists y φ$

Metamath Proof Explorer