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 ‘ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		spr0nelg	⊢ ∅ ∉ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }
2		sprssspr	⊢ ( Pairs ‘ 𝑉 ) ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }
3	2	sseli	⊢ ( ∅ ∈ ( Pairs ‘ 𝑉 ) → ∅ ∈ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } )
4	3	con3i	⊢ ( ¬ ∅ ∈ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } → ¬ ∅ ∈ ( Pairs ‘ 𝑉 ) )
5		df-nel	⊢ ( ∅ ∉ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } ↔ ¬ ∅ ∈ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } )
6		df-nel	⊢ ( ∅ ∉ ( Pairs ‘ 𝑉 ) ↔ ¬ ∅ ∈ ( Pairs ‘ 𝑉 ) )
7	4 5 6	3imtr4i	⊢ ( ∅ ∉ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } → ∅ ∉ ( Pairs ‘ 𝑉 ) )
8	1 7	ax-mp	⊢ ∅ ∉ ( Pairs ‘ 𝑉 )