Metamath Proof Explorer

Theorem spr0el

Description: The empty set is not an unordered pair over any set V . (Contributed by AV, 21-Nov-2021)

Ref Expression
Assertion spr0el ⊢ ∅ ∉ Pairs ⁡ V

Proof

Step Hyp Ref Expression
1 spr0nelg ⊢ ∅ ∉ p | ∃ a ∃ b p = a b
2 sprssspr ⊢ Pairs ⁡ V ⊆ p | ∃ a ∃ b p = a b
3 2 sseli ⊢ ∅ ∈ Pairs ⁡ V → ∅ ∈ p | ∃ a ∃ b p = a b
4 3 con3i ⊢ ¬ ∅ ∈ p | ∃ a ∃ b p = a b → ¬ ∅ ∈ Pairs ⁡ V
5 df-nel ⊢ ∅ ∉ p | ∃ a ∃ b p = a b ↔ ¬ ∅ ∈ p | ∃ a ∃ b p = a b
6 df-nel ⊢ ∅ ∉ Pairs ⁡ V ↔ ¬ ∅ ∈ Pairs ⁡ V
7 4 5 6 3imtr4i ⊢ ∅ ∉ p | ∃ a ∃ b p = a b → ∅ ∉ Pairs ⁡ V
8 1 7 ax-mp ⊢ ∅ ∉ Pairs ⁡ V