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	$$⊢\varnothing \subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg x\in \varnothing$$
2	1	pm2.21i	$$⊢x\in \varnothing \to x\in A$$
3	2	ssriv	$$⊢\varnothing \subseteq A$$