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 yX\subseteq y\leftrightarrow X=\varnothing$$

Proof

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