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 y X y X =

Proof

Step Hyp Ref Expression
1 0ex V
2 sseq2 y = X y X
3 ss0b X X =
4 2 3 bitrdi y = X y X =
5 1 4 spcv y X y X =
6 0ss y
7 6 ax-gen y y
8 sseq1 X = X y y
9 8 albidv X = y X y y y
10 7 9 mpbiri X = y X y
11 5 10 impbii y X y X =