Theorem ssn0 4354

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ≠ wne 2928   ⊆ wss 3902  ∅c0 4283

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-dif 3905  df-ss 3919  df-nul 4284

This theorem is referenced by:  unixp0  6230  frxp  8056  onfununi  8261  frmin  9639  carddomi2  9860  fin23lem21  10227  wunex2  10626  vdwmc2  16888  gsumval2  18591  subgint  19060  subrngint  20473  subrgint  20508  nzerooringczr  21415  hausnei2  23266  fbun  23753  fbfinnfr  23754  filuni  23798  isufil2  23821  ufileu  23832  filufint  23833  fmfnfm  23871  hausflim  23894  flimclslem  23897  fclsneii  23930  fclsbas  23934  fclsrest  23937  fclscf  23938  fclsfnflim  23940  flimfnfcls  23941  fclscmp  23943  ufilcmp  23945  isfcf  23947  fcfnei  23948  clssubg  24022  ustfilxp  24126  metustfbas  24470  restmetu  24483  reperflem  24732  metdseq0  24768  relcmpcmet  25243  bcthlem5  25253  minveclem4a  25355  dvlip  25923  wlkvtxiedg  29601  imadifxp  32576  constrextdg2lem  33756  bnj970  34954  neibastop1  36392  neibastop2  36394  heibor1lem  37848  isnumbasabl  43138  dfacbasgrp  43140  ioossioobi  45556  islptre  45658  stoweidlem35  46072  stoweidlem39  46076  fourierdlem46  46189