MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssn0 Structured version   Visualization version   GIF version

Theorem ssn0 4361
Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
ssn0 ((𝐴𝐵𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Proof of Theorem ssn0
StepHypRef Expression
1 sseq0 4360 . . . 4 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
21ex 417 . . 3 (𝐴𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
32necon3d 2981 . 2 (𝐴𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
43imp 411 1 ((𝐴𝐵𝐴 ≠ ∅) → 𝐵 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 400   = wceq 1563  wne 2960  wss 3907  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3910  df-ss 3924  df-nul 4289
This theorem is referenced by:  unixp0  6273  frxp  8110  onfununi  8316  frmin  9709  carddomi2  9944  fin23lem21  10311  wunex2  10711  vdwmc2  17027  gsumval2  18732  subgint  19205  subrngint  20633  subrgint  20668  nzerooringczr  21587  hausnei2  23467  fbun  23954  fbfinnfr  23955  filuni  23999  isufil2  24022  ufileu  24033  filufint  24034  fmfnfm  24072  hausflim  24095  flimclslem  24098  fclsneii  24131  fclsbas  24135  fclsrest  24138  fclscf  24139  fclsfnflim  24141  flimfnfcls  24142  fclscmp  24144  ufilcmp  24146  isfcf  24148  fcfnei  24149  clssubg  24223  ustfilxp  24327  metustfbas  24671  restmetu  24684  reperflem  24933  metdseq0  24969  relcmpcmet  25434  bcthlem5  25444  minveclem4a  25546  dvlip  26109  wlkvtxiedg  29879  imadifxp  32852  constrextdg2lem  34050  bnj970  35247  neibastop1  36727  neibastop2  36729  dfttc4  36898  elttcirr  36899  heibor1lem  38315  isnumbasabl  43690  dfacbasgrp  43692  ioossioobi  46092  islptre  46194  stoweidlem35  46608  stoweidlem39  46612  fourierdlem46  46725
  Copyright terms: Public domain W3C validator