Theorem ssn0 4340

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 4339	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 414	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2962	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539   ≠ wne 2941   ⊆ wss 3892  ∅c0 4262

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-v 3439  df-dif 3895  df-in 3899  df-ss 3909  df-nul 4263

This theorem is referenced by:  unixp0  6201  frxp  7998  onfununi  8203  frmin  9551  carddomi2  9772  fin23lem21  10141  wunex2  10540  vdwmc2  16725  gsumval2  18415  subgint  18824  subrgint  20091  hausnei2  22549  fbun  23036  fbfinnfr  23037  filuni  23081  isufil2  23104  ufileu  23115  filufint  23116  fmfnfm  23154  hausflim  23177  flimclslem  23180  fclsneii  23213  fclsbas  23217  fclsrest  23220  fclscf  23221  fclsfnflim  23223  flimfnfcls  23224  fclscmp  23226  ufilcmp  23228  isfcf  23230  fcfnei  23231  clssubg  23305  ustfilxp  23409  metustfbas  23758  restmetu  23771  reperflem  24026  metdseq0  24062  relcmpcmet  24527  bcthlem5  24537  minveclem4a  24639  dvlip  25202  wlkvtxiedg  28037  imadifxp  30985  bnj970  32972  neibastop1  34593  neibastop2  34595  heibor1lem  36011  isnumbasabl  40969  dfacbasgrp  40971  ioossioobi  43104  islptre  43209  stoweidlem35  43625  stoweidlem39  43629  fourierdlem46  43742  nzerooringczr  45688