Theorem ssn0 4351

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 4350	. . . 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 3899  ∅c0 4280

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 3902  df-ss 3916  df-nul 4281

This theorem is referenced by:  unixp0  6225  frxp  8050  onfununi  8255  frmin  9633  carddomi2  9854  fin23lem21  10221  wunex2  10620  vdwmc2  16878  gsumval2  18547  subgint  19016  subrngint  20429  subrgint  20464  nzerooringczr  21371  hausnei2  23222  fbun  23709  fbfinnfr  23710  filuni  23754  isufil2  23777  ufileu  23788  filufint  23789  fmfnfm  23827  hausflim  23850  flimclslem  23853  fclsneii  23886  fclsbas  23890  fclsrest  23893  fclscf  23894  fclsfnflim  23896  flimfnfcls  23897  fclscmp  23899  ufilcmp  23901  isfcf  23903  fcfnei  23904  clssubg  23978  ustfilxp  24082  metustfbas  24426  restmetu  24439  reperflem  24688  metdseq0  24724  relcmpcmet  25199  bcthlem5  25209  minveclem4a  25311  dvlip  25879  wlkvtxiedg  29557  imadifxp  32533  constrextdg2lem  33729  bnj970  34927  neibastop1  36350  neibastop2  36352  heibor1lem  37806  isnumbasabl  43096  dfacbasgrp  43098  ioossioobi  45514  islptre  45616  stoweidlem35  46030  stoweidlem39  46034  fourierdlem46  46147