Description: Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | opab0 | ⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opabn0 | ⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) | |
2 | df-ne | ⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ≠ ∅ ↔ ¬ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = ∅ ) | |
3 | 2exnaln | ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) | |
4 | 1 2 3 | 3bitr3i | ⊢ ( ¬ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = ∅ ↔ ¬ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) |
5 | 4 | con4bii | ⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) |