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 3443 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 119 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 ⊆ wss 3111 ∅c0 3404 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-dif 3113 df-in 3117 df-ss 3124 df-nul 3405 |
This theorem is referenced by: sseq0 3445 abf 3447 eq0rdv 3448 ssdisj 3460 0dif 3475 poirr2 4990 iotanul 5162 f00 5373 map0b 6644 phplem2 6810 php5dom 6820 sbthlem7 6919 fi0 6931 casefun 7041 caseinj 7045 djufun 7060 djuinj 7062 nnnninfeq 7083 exmidomni 7097 ixxdisj 9830 icodisj 9919 ioodisj 9920 uzdisj 10018 nn0disj 10063 fsum2dlemstep 11361 fprodssdc 11517 fprod2dlemstep 11549 ntrcls0 12672 |
Copyright terms: Public domain | W3C validator |