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  6274  frxp  8110  onfununi  8316  frmin  9709  carddomi2  9944  fin23lem21  10311  wunex2  10711  vdwmc2  17029  gsumval2  18734  subgint  19208  subrngint  20636  subrgint  20671  nzerooringczr  21590  hausnei2  23471  fbun  23958  fbfinnfr  23959  filuni  24003  isufil2  24026  ufileu  24037  filufint  24038  fmfnfm  24076  hausflim  24099  flimclslem  24102  fclsneii  24135  fclsbas  24139  fclsrest  24142  fclscf  24143  fclsfnflim  24145  flimfnfcls  24146  fclscmp  24148  ufilcmp  24150  isfcf  24152  fcfnei  24153  clssubg  24227  ustfilxp  24331  metustfbas  24675  restmetu  24688  reperflem  24937  metdseq0  24973  relcmpcmet  25438  bcthlem5  25448  minveclem4a  25550  dvlip  26113  wlkvtxiedg  29883  imadifxp  32856  constrextdg2lem  34055  bnj970  35252  neibastop1  36732  neibastop2  36734  dfttc4  36903  elttcirr  36904  heibor1lem  38320  isnumbasabl  43695  dfacbasgrp  43697  ioossioobi  46091  islptre  46193  stoweidlem35  46607  stoweidlem39  46611  fourierdlem46  46724