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 4350 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | |
2 | 1 | ex 413 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅)) |
3 | 2 | necon3d 3034 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅)) |
4 | 3 | imp 407 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ≠ wne 3013 ⊆ wss 3933 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-ne 3014 df-dif 3936 df-in 3940 df-ss 3949 df-nul 4289 |
This theorem is referenced by: unixp0 6127 frxp 7809 onfununi 7967 carddomi2 9387 fin23lem21 9749 wunex2 10148 vdwmc2 16303 gsumval2 17884 subgint 18241 subrgint 19486 hausnei2 21889 fbun 22376 fbfinnfr 22377 filuni 22421 isufil2 22444 ufileu 22455 filufint 22456 fmfnfm 22494 hausflim 22517 flimclslem 22520 fclsneii 22553 fclsbas 22557 fclsrest 22560 fclscf 22561 fclsfnflim 22563 flimfnfcls 22564 fclscmp 22566 ufilcmp 22568 isfcf 22570 fcfnei 22571 clssubg 22644 ustfilxp 22748 metustfbas 23094 restmetu 23107 reperflem 23353 metdseq0 23389 relcmpcmet 23848 bcthlem5 23858 minveclem4a 23960 dvlip 24517 wlkvtxiedg 27333 imadifxp 30279 bnj970 32118 frmin 32981 neibastop1 33604 neibastop2 33606 heibor1lem 34968 isnumbasabl 39584 dfacbasgrp 39586 ioossioobi 41669 islptre 41776 stoweidlem35 42197 stoweidlem39 42201 fourierdlem46 42314 nzerooringczr 44271 |
Copyright terms: Public domain | W3C validator |