Theorem ssn0 4361

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 4360	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 417	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2981	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 411	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ≠ wne 2960   ⊆ wss 3907  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3910  df-ss 3924  df-nul 4289

This theorem is referenced by:  unixp0  6273  frxp  8110  onfununi  8316  frmin  9709  carddomi2  9944  fin23lem21  10311  wunex2  10711  vdwmc2  17027  gsumval2  18732  subgint  19205  subrngint  20633  subrgint  20668  nzerooringczr  21587  hausnei2  23467  fbun  23954  fbfinnfr  23955  filuni  23999  isufil2  24022  ufileu  24033  filufint  24034  fmfnfm  24072  hausflim  24095  flimclslem  24098  fclsneii  24131  fclsbas  24135  fclsrest  24138  fclscf  24139  fclsfnflim  24141  flimfnfcls  24142  fclscmp  24144  ufilcmp  24146  isfcf  24148  fcfnei  24149  clssubg  24223  ustfilxp  24327  metustfbas  24671  restmetu  24684  reperflem  24933  metdseq0  24969  relcmpcmet  25434  bcthlem5  25444  minveclem4a  25546  dvlip  26109  wlkvtxiedg  29879  imadifxp  32852  constrextdg2lem  34050  bnj970  35247  neibastop1  36727  neibastop2  36729  dfttc4  36898  elttcirr  36899  heibor1lem  38315  isnumbasabl  43690  dfacbasgrp  43692  ioossioobi  46092  islptre  46194  stoweidlem35  46608  stoweidlem39  46612  fourierdlem46  46725