Metamath Proof Explorer


Theorem opab0

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

Ref Expression
Assertion opab0 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅ ↔ ∀ 𝑥𝑦 ¬ 𝜑 )

Proof

Step Hyp Ref Expression
1 opabn0 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥𝑦 𝜑 )
2 df-ne ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ≠ ∅ ↔ ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅ )
3 2exnaln ( ∃ 𝑥𝑦 𝜑 ↔ ¬ ∀ 𝑥𝑦 ¬ 𝜑 )
4 1 2 3 3bitr3i ( ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅ ↔ ¬ ∀ 𝑥𝑦 ¬ 𝜑 )
5 4 con4bii ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅ ↔ ∀ 𝑥𝑦 ¬ 𝜑 )