Theorem ss0b

Description: Any subset of the empty set is empty. Theorem 5 of Suppes p. 23 and its converse. (Contributed by NM, 17-Sep-2003)

	Ref	Expression
Assertion	ss0b	⊢ ( 𝐴 ⊆ ∅ ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝐴
2		eqss	⊢ ( 𝐴 = ∅ ↔ ( 𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴 ) )
3	1 2	mpbiran2	⊢ ( 𝐴 = ∅ ↔ 𝐴 ⊆ ∅ )
4	3	bicomi	⊢ ( 𝐴 ⊆ ∅ ↔ 𝐴 = ∅ )