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