opab0

Description: Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021)

		Ref	Expression
	Assertion	opab0	$⊢ \{⟨x, y⟩ \| φ\} = \emptyset \leftrightarrow \forall x \forall y \neg φ$

Step	Hyp	Ref	Expression
1		opabn0	$⊢ \{⟨x, y⟩ \| φ\} \neq \emptyset \leftrightarrow \exists x \exists y φ$
2		df-ne	$⊢ \{⟨x, y⟩ \| φ\} \neq \emptyset \leftrightarrow \neg \{⟨x, y⟩ \| φ\} = \emptyset$
3		2exnaln	$⊢ \exists x \exists y φ \leftrightarrow \neg \forall x \forall y \neg φ$
4	1 2 3	3bitr3i	$⊢ \neg \{⟨x, y⟩ \| φ\} = \emptyset \leftrightarrow \neg \forall x \forall y \neg φ$
5	4	con4bii	$⊢ \{⟨x, y⟩ \| φ\} = \emptyset \leftrightarrow \forall x \forall y \neg φ$

Metamath Proof Explorer