Theorem ssn0 4399

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 4398	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 413	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2961	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ≠ wne 2940   ⊆ wss 3947  ∅c0 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  unixp0  6279  frxp  8108  onfununi  8337  frmin  9740  carddomi2  9961  fin23lem21  10330  wunex2  10729  vdwmc2  16908  gsumval2  18601  subgint  19024  subrgint  20378  hausnei2  22848  fbun  23335  fbfinnfr  23336  filuni  23380  isufil2  23403  ufileu  23414  filufint  23415  fmfnfm  23453  hausflim  23476  flimclslem  23479  fclsneii  23512  fclsbas  23516  fclsrest  23519  fclscf  23520  fclsfnflim  23522  flimfnfcls  23523  fclscmp  23525  ufilcmp  23527  isfcf  23529  fcfnei  23530  clssubg  23604  ustfilxp  23708  metustfbas  24057  restmetu  24070  reperflem  24325  metdseq0  24361  relcmpcmet  24826  bcthlem5  24836  minveclem4a  24938  dvlip  25501  wlkvtxiedg  28871  imadifxp  31819  bnj970  33946  neibastop1  35232  neibastop2  35234  heibor1lem  36665  isnumbasabl  41833  dfacbasgrp  41835  ioossioobi  44216  islptre  44321  stoweidlem35  44737  stoweidlem39  44741  fourierdlem46  44854  subrngint  46723  nzerooringczr  46923