Theorem ssn0 4368

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ≠ wne 2964   ⊆ wss 3913  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-dif 3916  df-ss 3930  df-nul 4295

This theorem is referenced by:  unixp0  6285  frxp  8122  onfununi  8328  frmin  9721  carddomi2  9956  fin23lem21  10323  wunex2  10723  vdwmc2  17039  gsumval2  18744  subgint  19217  subrngint  20645  subrgint  20680  nzerooringczr  21599  hausnei2  23479  fbun  23966  fbfinnfr  23967  filuni  24011  isufil2  24034  ufileu  24045  filufint  24046  fmfnfm  24084  hausflim  24107  flimclslem  24110  fclsneii  24143  fclsbas  24147  fclsrest  24150  fclscf  24151  fclsfnflim  24153  flimfnfcls  24154  fclscmp  24156  ufilcmp  24158  isfcf  24160  fcfnei  24161  clssubg  24235  ustfilxp  24339  metustfbas  24683  restmetu  24696  reperflem  24945  metdseq0  24981  relcmpcmet  25446  bcthlem5  25456  minveclem4a  25558  dvlip  26121  wlkvtxiedg  29915  imadifxp  32887  constrextdg2lem  34083  bnj970  35280  neibastop1  36793  neibastop2  36795  dfttc4  36964  elttcirr  36965  heibor1lem  38382  isnumbasabl  43759  dfacbasgrp  43761  ioossioobi  46159  islptre  46261  stoweidlem35  46675  stoweidlem39  46679  fourierdlem46  46792