|   | 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 4402 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | |
| 2 | 1 | ex 412 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅)) | 
| 3 | 2 | necon3d 2960 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅)) | 
| 4 | 3 | imp 406 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ≠ wne 2939 ⊆ wss 3950 ∅c0 4332 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ne 2940 df-dif 3953 df-ss 3967 df-nul 4333 | 
| This theorem is referenced by: unixp0 6302 frxp 8152 onfununi 8382 frmin 9790 carddomi2 10011 fin23lem21 10380 wunex2 10779 vdwmc2 17018 gsumval2 18700 subgint 19169 subrngint 20561 subrgint 20596 nzerooringczr 21492 hausnei2 23362 fbun 23849 fbfinnfr 23850 filuni 23894 isufil2 23917 ufileu 23928 filufint 23929 fmfnfm 23967 hausflim 23990 flimclslem 23993 fclsneii 24026 fclsbas 24030 fclsrest 24033 fclscf 24034 fclsfnflim 24036 flimfnfcls 24037 fclscmp 24039 ufilcmp 24041 isfcf 24043 fcfnei 24044 clssubg 24118 ustfilxp 24222 metustfbas 24571 restmetu 24584 reperflem 24841 metdseq0 24877 relcmpcmet 25353 bcthlem5 25363 minveclem4a 25465 dvlip 26033 wlkvtxiedg 29644 imadifxp 32615 constrextdg2lem 33790 bnj970 34962 neibastop1 36361 neibastop2 36363 heibor1lem 37817 isnumbasabl 43123 dfacbasgrp 43125 ioossioobi 45535 islptre 45639 stoweidlem35 46055 stoweidlem39 46059 fourierdlem46 46172 | 
| Copyright terms: Public domain | W3C validator |