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	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )