Metamath Proof Explorer
Description: Any subset of the empty set is empty. Dual of vss . 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 |
|