Theorem ssn0 4363

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ≠ wne 2958   ⊆ wss 3906  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 3909  df-ss 3923  df-nul 4288

This theorem is referenced by:  unixp0  6286  frxp  8123  onfununi  8329  frmin  9722  carddomi2  9957  fin23lem21  10324  wunex2  10724  vdwmc2  17040  gsumval2  18745  subgint  19218  subrngint  20646  subrgint  20681  nzerooringczr  21611  hausnei2  23491  fbun  23978  fbfinnfr  23979  filuni  24023  isufil2  24046  ufileu  24057  filufint  24058  fmfnfm  24096  hausflim  24119  flimclslem  24122  fclsneii  24155  fclsbas  24159  fclsrest  24162  fclscf  24163  fclsfnflim  24165  flimfnfcls  24166  fclscmp  24168  ufilcmp  24170  isfcf  24172  fcfnei  24173  clssubg  24247  ustfilxp  24351  metustfbas  24695  restmetu  24708  reperflem  24957  metdseq0  24993  relcmpcmet  25458  bcthlem5  25468  minveclem4a  25570  dvlip  26133  wlkvtxiedg  29955  imadifxp  32927  constrextdg2lem  34119  bnj970  35316  neibastop1  36851  neibastop2  36853  dfttc4  37022  elttcirr  37023  heibor1lem  38441  isnumbasabl  43816  dfacbasgrp  43818  ioossioobi  46216  islptre  46318  stoweidlem35  46732  stoweidlem39  46736  fourierdlem46  46849