Theorem ssn0 4354

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 4353	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 418	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2976	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 412	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ≠ wne 2955   ⊆ wss 3895  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ss 3896  df-dif 4047  df-nul 4279

This theorem is used by:  unixp0  6286  frxp  8141  onfununi  8353  frmin  9757  carddomi2  10055  fin23lem21  10421  wunex2  10827  vdwmc2  17163  gsumval2  18881  subgint  19367  subrngint  20818  subrgint  20853  nzerooringczr  21792  hausnei2  23677  fbun  24165  fbfinnfr  24166  filuni  24210  isufil2  24233  ufileu  24244  filufint  24245  fmfnfm  24283  hausflim  24306  flimclslem  24309  fclsneii  24342  fclsbas  24346  fclsrest  24349  fclscf  24350  fclsfnflim  24352  flimfnfcls  24353  fclscmp  24355  ufilcmp  24357  isfcf  24359  fcfnei  24360  clssubg  24434  ustfilxp  24538  metustfbas  24882  restmetu  24895  reperflem  25144  metdseq0  25180  relcmpcmet  25645  bcthlem5  25655  minveclem4a  25757  dvlip  26319  wlkvtxiedg  30211  imadifxp  33243  constrextdg2lem  34427  bnj970  35624  neibastop1  37240  neibastop2  37242  dfttc4  37411  elttcirr  37412  heibor1lem  38837  isnumbasabl  44202  dfacbasgrp  44204  ioossioobi  46623  islptre  46725  stoweidlem35  47139  stoweidlem39  47143  fourierdlem46  47256