Theorem ssn0 4358

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ≠ wne 2933   ⊆ wss 3903  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3906  df-ss 3920  df-nul 4288

This theorem is referenced by:  unixp0  6249  frxp  8078  onfununi  8283  frmin  9673  carddomi2  9894  fin23lem21  10261  wunex2  10661  vdwmc2  16919  gsumval2  18623  subgint  19092  subrngint  20505  subrgint  20540  nzerooringczr  21447  hausnei2  23309  fbun  23796  fbfinnfr  23797  filuni  23841  isufil2  23864  ufileu  23875  filufint  23876  fmfnfm  23914  hausflim  23937  flimclslem  23940  fclsneii  23973  fclsbas  23977  fclsrest  23980  fclscf  23981  fclsfnflim  23983  flimfnfcls  23984  fclscmp  23986  ufilcmp  23988  isfcf  23990  fcfnei  23991  clssubg  24065  ustfilxp  24169  metustfbas  24513  restmetu  24526  reperflem  24775  metdseq0  24811  relcmpcmet  25286  bcthlem5  25296  minveclem4a  25398  dvlip  25966  wlkvtxiedg  29710  imadifxp  32687  constrextdg2lem  33925  bnj970  35122  neibastop1  36572  neibastop2  36574  heibor1lem  38054  isnumbasabl  43457  dfacbasgrp  43459  ioossioobi  45871  islptre  45973  stoweidlem35  46387  stoweidlem39  46391  fourierdlem46  46504