![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ss0 | GIF version |
Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.) |
Ref | Expression |
---|---|
ss0 | ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss0b 3307 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 118 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1287 ⊆ wss 2986 ∅c0 3272 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 |
This theorem depends on definitions: df-bi 115 df-tru 1290 df-nf 1393 df-sb 1690 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-v 2616 df-dif 2988 df-in 2992 df-ss 2999 df-nul 3273 |
This theorem is referenced by: sseq0 3309 abf 3311 eq0rdv 3312 ssdisj 3324 0dif 3339 poirr2 4782 iotanul 4952 f00 5153 map0b 6377 phplem2 6502 php5dom 6512 sbthlem7 6593 casefun 6697 caseinj 6701 djufun 6705 djuinj 6707 exmidomni 6719 ixxdisj 9230 icodisj 9318 ioodisj 9319 uzdisj 9414 nn0disj 9453 nninfalllemn 11254 |
Copyright terms: Public domain | W3C validator |