Theorem ssn0 4353

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ≠ wne 2929   ⊆ wss 3898  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-dif 3901  df-ss 3915  df-nul 4283

This theorem is referenced by:  unixp0  6235  frxp  8062  onfununi  8267  frmin  9649  carddomi2  9870  fin23lem21  10237  wunex2  10636  vdwmc2  16893  gsumval2  18596  subgint  19065  subrngint  20477  subrgint  20512  nzerooringczr  21419  hausnei2  23269  fbun  23756  fbfinnfr  23757  filuni  23801  isufil2  23824  ufileu  23835  filufint  23836  fmfnfm  23874  hausflim  23897  flimclslem  23900  fclsneii  23933  fclsbas  23937  fclsrest  23940  fclscf  23941  fclsfnflim  23943  flimfnfcls  23944  fclscmp  23946  ufilcmp  23948  isfcf  23950  fcfnei  23951  clssubg  24025  ustfilxp  24129  metustfbas  24473  restmetu  24486  reperflem  24735  metdseq0  24771  relcmpcmet  25246  bcthlem5  25256  minveclem4a  25358  dvlip  25926  wlkvtxiedg  29605  imadifxp  32583  constrextdg2lem  33782  bnj970  34980  neibastop1  36424  neibastop2  36426  heibor1lem  37869  isnumbasabl  43223  dfacbasgrp  43225  ioossioobi  45641  islptre  45743  stoweidlem35  46157  stoweidlem39  46161  fourierdlem46  46274