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 
|- (/) e/ { p | E. a E. b p = { a , b } }

Proof

Step Hyp Ref Expression
1 ianor 
 |-  ( -. ( p = (/) /\ E. a E. b p = { a , b } ) <-> ( -. p = (/) \/ -. E. a E. b p = { a , b } ) )
2 1 bicomi 
 |-  ( ( -. p = (/) \/ -. E. a E. b p = { a , b } ) <-> -. ( p = (/) /\ E. a E. b p = { a , b } ) )
3 2 albii 
 |-  ( A. p ( -. p = (/) \/ -. E. a E. b p = { a , b } ) <-> A. p -. ( p = (/) /\ E. a E. b p = { a , b } ) )
4 alnex 
 |-  ( A. p -. ( p = (/) /\ E. a E. b p = { a , b } ) <-> -. E. p ( p = (/) /\ E. a E. b p = { a , b } ) )
5 3 4 bitri 
 |-  ( A. p ( -. p = (/) \/ -. E. a E. b p = { a , b } ) <-> -. E. p ( p = (/) /\ E. a E. b p = { a , b } ) )
6 vex 
 |-  a e. _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. a A. b -. p = { a , b } )
12 2nexaln 
 |-  ( -. E. a E. b p = { a , b } <-> A. a A. b -. p = { a , b } )
13 11 12 sylibr 
 |-  ( p = (/) -> -. E. a E. b p = { a , b } )
14 13 imori 
 |-  ( -. p = (/) \/ -. E. a E. b p = { a , b } )
15 5 14 mpgbi 
 |-  -. E. p ( p = (/) /\ E. a E. b p = { a , b } )
16 df-nel 
 |-  ( (/) e/ { p | E. a E. b p = { a , b } } <-> -. (/) e. { p | E. a E. b p = { a , b } } )
17 clelab 
 |-  ( (/) e. { p | E. a E. b p = { a , b } } <-> E. p ( p = (/) /\ E. a E. b p = { a , b } ) )
18 16 17 xchbinx 
 |-  ( (/) e/ { p | E. a E. b p = { a , b } } <-> -. E. p ( p = (/) /\ E. a E. b p = { a , b } ) )
19 15 18 mpbir 
 |-  (/) e/ { p | E. a E. b p = { a , b } }