Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssn0 | Structured version Visualization version GIF version |
Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.) |
Ref | Expression |
---|---|
ssn0 | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq0 4314 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | |
2 | 1 | ex 416 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅)) |
3 | 2 | necon3d 2961 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅)) |
4 | 3 | imp 410 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ≠ wne 2940 ⊆ wss 3866 ∅c0 4237 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-v 3410 df-dif 3869 df-in 3873 df-ss 3883 df-nul 4238 |
This theorem is referenced by: unixp0 6146 frxp 7893 onfununi 8078 frmin 9365 carddomi2 9586 fin23lem21 9953 wunex2 10352 vdwmc2 16532 gsumval2 18158 subgint 18567 subrgint 19822 hausnei2 22250 fbun 22737 fbfinnfr 22738 filuni 22782 isufil2 22805 ufileu 22816 filufint 22817 fmfnfm 22855 hausflim 22878 flimclslem 22881 fclsneii 22914 fclsbas 22918 fclsrest 22921 fclscf 22922 fclsfnflim 22924 flimfnfcls 22925 fclscmp 22927 ufilcmp 22929 isfcf 22931 fcfnei 22932 clssubg 23006 ustfilxp 23110 metustfbas 23455 restmetu 23468 reperflem 23715 metdseq0 23751 relcmpcmet 24215 bcthlem5 24225 minveclem4a 24327 dvlip 24890 wlkvtxiedg 27712 imadifxp 30659 bnj970 32640 neibastop1 34285 neibastop2 34287 heibor1lem 35704 isnumbasabl 40634 dfacbasgrp 40636 ioossioobi 42730 islptre 42835 stoweidlem35 43251 stoweidlem39 43255 fourierdlem46 43368 nzerooringczr 45303 |
Copyright terms: Public domain | W3C validator |