Theorem 0ss

Description: The empty set is a subset of any class. Dual of ssv . Part of Exercise 1 of TakeutiZaring p. 22. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Assertion	0ss	⊢ ∅ ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i	⊢ ( 𝑥 ∈ ∅ → 𝑥 ∈ 𝐴 )
3	2	ssriv	⊢ ∅ ⊆ 𝐴