Metamath Proof Explorer

Theorem vsn

Description: The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion vsn 
|- { _V } = (/)

Proof

Step Hyp Ref Expression
1 vprc 
 |-  -. _V e. _V
2 snprc 
 |-  ( -. _V e. _V <-> { _V } = (/) )
3 1 2 mpbi 
 |-  { _V } = (/)