This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opabf

Description: A class abstraction of a collection of ordered pairs with a negated wff is the empty set. (Contributed by Peter Mazsa, 21-Oct-2019) (Proof shortened by Thierry Arnoux, 18-Feb-2022)

		Ref	Expression
	Hypothesis	opabf.1	$⊢ \neg φ$
	Assertion	opabf	$⊢ \{⟨x, y⟩ \| φ\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		opabf.1	$⊢ \neg φ$
2	1	gen2	$⊢ \forall x \forall y \neg φ$
3		opab0	$⊢ \{⟨x, y⟩ \| φ\} = \emptyset \leftrightarrow \forall x \forall y \neg φ$
4	2 3	mpbir	$⊢ \{⟨x, y⟩ \| φ\} = \emptyset$