Theorem spr0nelg

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

	Ref	Expression
Assertion	spr0nelg	⊢ ∅ ∉ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }

Proof

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