Theorem ssn0 4356

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ≠ wne 2932   ⊆ wss 3901  ∅c0 4285

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3904  df-ss 3918  df-nul 4286

This theorem is referenced by:  unixp0  6241  frxp  8068  onfununi  8273  frmin  9661  carddomi2  9882  fin23lem21  10249  wunex2  10649  vdwmc2  16907  gsumval2  18611  subgint  19080  subrngint  20493  subrgint  20528  nzerooringczr  21435  hausnei2  23297  fbun  23784  fbfinnfr  23785  filuni  23829  isufil2  23852  ufileu  23863  filufint  23864  fmfnfm  23902  hausflim  23925  flimclslem  23928  fclsneii  23961  fclsbas  23965  fclsrest  23968  fclscf  23969  fclsfnflim  23971  flimfnfcls  23972  fclscmp  23974  ufilcmp  23976  isfcf  23978  fcfnei  23979  clssubg  24053  ustfilxp  24157  metustfbas  24501  restmetu  24514  reperflem  24763  metdseq0  24799  relcmpcmet  25274  bcthlem5  25284  minveclem4a  25386  dvlip  25954  wlkvtxiedg  29698  imadifxp  32676  constrextdg2lem  33905  bnj970  35103  neibastop1  36553  neibastop2  36555  heibor1lem  38006  isnumbasabl  43344  dfacbasgrp  43346  ioossioobi  45759  islptre  45861  stoweidlem35  46275  stoweidlem39  46279  fourierdlem46  46392