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 \phi$$
Assertion	opabf	$$⊢\left\{⟨x,y⟩|\phi \right\}=\varnothing$$

Proof

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