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	⊢ ¬ 𝜑
	Assertion	opabf	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅

Proof

Step	Hyp	Ref	Expression
1		opabf.1	⊢ ¬ 𝜑
2	1	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑
3		opab0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )
4	2 3	mpbir	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅