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	⊢ ( ∀ 𝑦 𝑋 ⊆ 𝑦 ↔ 𝑋 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		sseq2	⊢ ( 𝑦 = ∅ → ( 𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ ∅ ) )
3		ss0b	⊢ ( 𝑋 ⊆ ∅ ↔ 𝑋 = ∅ )
4	2 3	bitrdi	⊢ ( 𝑦 = ∅ → ( 𝑋 ⊆ 𝑦 ↔ 𝑋 = ∅ ) )
5	1 4	spcv	⊢ ( ∀ 𝑦 𝑋 ⊆ 𝑦 → 𝑋 = ∅ )
6		0ss	⊢ ∅ ⊆ 𝑦
7	6	ax-gen	⊢ ∀ 𝑦 ∅ ⊆ 𝑦
8		sseq1	⊢ ( 𝑋 = ∅ → ( 𝑋 ⊆ 𝑦 ↔ ∅ ⊆ 𝑦 ) )
9	8	albidv	⊢ ( 𝑋 = ∅ → ( ∀ 𝑦 𝑋 ⊆ 𝑦 ↔ ∀ 𝑦 ∅ ⊆ 𝑦 ) )
10	7 9	mpbiri	⊢ ( 𝑋 = ∅ → ∀ 𝑦 𝑋 ⊆ 𝑦 )
11	5 10	impbii	⊢ ( ∀ 𝑦 𝑋 ⊆ 𝑦 ↔ 𝑋 = ∅ )