Theorem ssn0 4357

Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)

Assertion

Ref	Expression
ssn0	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Proof of Theorem ssn0

Step	Hyp	Ref	Expression
1		sseq0 4356	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 416	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2977	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 410	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ≠ wne 2956   ⊆ wss 3904  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3907  df-ss 3921  df-nul 4286

This theorem is referenced by:  unixp0  6266  frxp  8101  onfununi  8307  frmin  9704  carddomi2  9925  fin23lem21  10293  wunex2  10693  vdwmc2  16998  gsumval2  18703  subgint  19175  subrngint  20589  subrgint  20624  nzerooringczr  21512  hausnei2  23393  fbun  23880  fbfinnfr  23881  filuni  23925  isufil2  23948  ufileu  23959  filufint  23960  fmfnfm  23998  hausflim  24021  flimclslem  24024  fclsneii  24057  fclsbas  24061  fclsrest  24064  fclscf  24065  fclsfnflim  24067  flimfnfcls  24068  fclscmp  24070  ufilcmp  24072  isfcf  24074  fcfnei  24075  clssubg  24149  ustfilxp  24253  metustfbas  24597  restmetu  24610  reperflem  24859  metdseq0  24895  relcmpcmet  25360  bcthlem5  25370  minveclem4a  25472  dvlip  26035  wlkvtxiedg  29771  imadifxp  32750  constrextdg2lem  34006  bnj970  35206  neibastop1  36683  neibastop2  36685  dfttc4  36854  elttcirr  36855  heibor1lem  38272  isnumbasabl  43647  dfacbasgrp  43649  ioossioobi  46057  islptre  46159  stoweidlem35  46573  stoweidlem39  46577  fourierdlem46  46690