Metamath Proof Explorer

Theorem al0ssb

Description: The empty set is the unique class which is a subclass of any set. (Contributed by AV, 24-Aug-2022)

Ref Expression
Assertion al0ssb 
|- ( A. y X C_ y <-> X = (/) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 sseq2 
 |-  ( y = (/) -> ( X C_ y <-> X C_ (/) ) )
3 ss0b 
 |-  ( X C_ (/) <-> X = (/) )
4 2 3 bitrdi 
 |-  ( y = (/) -> ( X C_ y <-> X = (/) ) )
5 1 4 spcv 
 |-  ( A. y X C_ y -> X = (/) )
6 0ss 
 |-  (/) C_ y
7 6 ax-gen 
 |-  A. y (/) C_ y
8 sseq1 
 |-  ( X = (/) -> ( X C_ y <-> (/) C_ y ) )
9 8 albidv 
 |-  ( X = (/) -> ( A. y X C_ y <-> A. y (/) C_ y ) )
10 7 9 mpbiri 
 |-  ( X = (/) -> A. y X C_ y )
11 5 10 impbii 
 |-  ( A. y X C_ y <-> X = (/) )