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 412	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2946	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3905  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-dif 3908  df-ss 3922  df-nul 4287

This theorem is referenced by:  unixp0  6235  frxp  8066  onfununi  8271  frmin  9664  carddomi2  9885  fin23lem21  10252  wunex2  10651  vdwmc2  16909  gsumval2  18578  subgint  19047  subrngint  20463  subrgint  20498  nzerooringczr  21405  hausnei2  23256  fbun  23743  fbfinnfr  23744  filuni  23788  isufil2  23811  ufileu  23822  filufint  23823  fmfnfm  23861  hausflim  23884  flimclslem  23887  fclsneii  23920  fclsbas  23924  fclsrest  23927  fclscf  23928  fclsfnflim  23930  flimfnfcls  23931  fclscmp  23933  ufilcmp  23935  isfcf  23937  fcfnei  23938  clssubg  24012  ustfilxp  24116  metustfbas  24461  restmetu  24474  reperflem  24723  metdseq0  24759  relcmpcmet  25234  bcthlem5  25244  minveclem4a  25346  dvlip  25914  wlkvtxiedg  29588  imadifxp  32563  constrextdg2lem  33714  bnj970  34913  neibastop1  36332  neibastop2  36334  heibor1lem  37788  isnumbasabl  43079  dfacbasgrp  43081  ioossioobi  45499  islptre  45601  stoweidlem35  46017  stoweidlem39  46021  fourierdlem46  46134