# 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 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{X}\subseteq {y}↔{X}=\varnothing$

### Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 sseq2 ${⊢}{y}=\varnothing \to \left({X}\subseteq {y}↔{X}\subseteq \varnothing \right)$
3 ss0b ${⊢}{X}\subseteq \varnothing ↔{X}=\varnothing$
4 2 3 syl6bb ${⊢}{y}=\varnothing \to \left({X}\subseteq {y}↔{X}=\varnothing \right)$
5 1 4 spcv ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{X}\subseteq {y}\to {X}=\varnothing$
6 0ss ${⊢}\varnothing \subseteq {y}$
7 6 ax-gen ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\varnothing \subseteq {y}$
8 sseq1 ${⊢}{X}=\varnothing \to \left({X}\subseteq {y}↔\varnothing \subseteq {y}\right)$
9 8 albidv ${⊢}{X}=\varnothing \to \left(\forall {y}\phantom{\rule{.4em}{0ex}}{X}\subseteq {y}↔\forall {y}\phantom{\rule{.4em}{0ex}}\varnothing \subseteq {y}\right)$
10 7 9 mpbiri ${⊢}{X}=\varnothing \to \forall {y}\phantom{\rule{.4em}{0ex}}{X}\subseteq {y}$
11 5 10 impbii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{X}\subseteq {y}↔{X}=\varnothing$