Metamath Proof Explorer

Theorem spr0nelg

Description: The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021)

Ref Expression
Assertion spr0nelg ⊢ ∅ ∉ p | ∃ a ∃ b p = a b

Proof

Step Hyp Ref Expression
1 ianor ⊢ ¬ p = ∅ ∧ ∃ a ∃ b p = a b ↔ ¬ p = ∅ ∨ ¬ ∃ a ∃ b p = a b
2 1 bicomi ⊢ ¬ p = ∅ ∨ ¬ ∃ a ∃ b p = a b ↔ ¬ p = ∅ ∧ ∃ a ∃ b p = a b
3 2 albii ⊢ ∀ p ¬ p = ∅ ∨ ¬ ∃ a ∃ b p = a b ↔ ∀ p ¬ p = ∅ ∧ ∃ a ∃ b p = a b
4 alnex ⊢ ∀ p ¬ p = ∅ ∧ ∃ a ∃ b p = a b ↔ ¬ ∃ p p = ∅ ∧ ∃ a ∃ b p = a b
5 3 4 bitri ⊢ ∀ p ¬ p = ∅ ∨ ¬ ∃ a ∃ b p = a b ↔ ¬ ∃ p p = ∅ ∧ ∃ a ∃ b p = a b
6 vex ⊢ a ∈ V
7 6 prnz ⊢ a b ≠ ∅
8 7 nesymi ⊢ ¬ ∅ = a b
9 eqeq1 ⊢ p = ∅ → p = a b ↔ ∅ = a b
10 8 9 mtbiri ⊢ p = ∅ → ¬ p = a b
11 10 alrimivv ⊢ p = ∅ → ∀ a ∀ b ¬ p = a b
12 2nexaln ⊢ ¬ ∃ a ∃ b p = a b ↔ ∀ a ∀ b ¬ p = a b
13 11 12 sylibr ⊢ p = ∅ → ¬ ∃ a ∃ b p = a b
14 13 imori ⊢ ¬ p = ∅ ∨ ¬ ∃ a ∃ b p = a b
15 5 14 mpgbi ⊢ ¬ ∃ p p = ∅ ∧ ∃ a ∃ b p = a b
16 df-nel ⊢ ∅ ∉ p | ∃ a ∃ b p = a b ↔ ¬ ∅ ∈ p | ∃ a ∃ b p = a b
17 clelab ⊢ ∅ ∈ p | ∃ a ∃ b p = a b ↔ ∃ p p = ∅ ∧ ∃ a ∃ b p = a b
18 16 17 xchbinx ⊢ ∅ ∉ p | ∃ a ∃ b p = a b ↔ ¬ ∃ p p = ∅ ∧ ∃ a ∃ b p = a b
19 15 18 mpbir ⊢ ∅ ∉ p | ∃ a ∃ b p = a b