Theorem ssn0 4358

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2957   ⊆ wss 3902  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-dif 3905  df-ss 3919  df-nul 4283

This theorem is used by:  unixp0  6285  frxp  8128  onfununi  8334  frmin  9735  carddomi2  9979  fin23lem21  10345  wunex2  10751  vdwmc2  17077  gsumval2  18794  subgint  19280  subrngint  20728  subrgint  20763  nzerooringczr  21699  hausnei2  23584  fbun  24072  fbfinnfr  24073  filuni  24117  isufil2  24140  ufileu  24151  filufint  24152  fmfnfm  24190  hausflim  24213  flimclslem  24216  fclsneii  24249  fclsbas  24253  fclsrest  24256  fclscf  24257  fclsfnflim  24259  flimfnfcls  24260  fclscmp  24262  ufilcmp  24264  isfcf  24266  fcfnei  24267  clssubg  24341  ustfilxp  24445  metustfbas  24789  restmetu  24802  reperflem  25051  metdseq0  25087  relcmpcmet  25552  bcthlem5  25562  minveclem4a  25664  dvlip  26227  wlkvtxiedg  30092  imadifxp  33082  constrextdg2lem  34266  bnj970  35464  neibastop1  36986  neibastop2  36988  dfttc4  37157  elttcirr  37158  heibor1lem  38567  isnumbasabl  43955  dfacbasgrp  43957  ioossioobi  46355  islptre  46457  stoweidlem35  46871  stoweidlem39  46875  fourierdlem46  46988