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

Theorem ssn0 4403
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 4402 . . . 4 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
21ex 412 . . 3 (𝐴𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
32necon3d 2960 . 2 (𝐴𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
43imp 406 1 ((𝐴𝐵𝐴 ≠ ∅) → 𝐵 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1539  wne 2939  wss 3950  c0 4332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-dif 3953  df-ss 3967  df-nul 4333
This theorem is referenced by:  unixp0  6302  frxp  8152  onfununi  8382  frmin  9790  carddomi2  10011  fin23lem21  10380  wunex2  10779  vdwmc2  17018  gsumval2  18700  subgint  19169  subrngint  20561  subrgint  20596  nzerooringczr  21492  hausnei2  23362  fbun  23849  fbfinnfr  23850  filuni  23894  isufil2  23917  ufileu  23928  filufint  23929  fmfnfm  23967  hausflim  23990  flimclslem  23993  fclsneii  24026  fclsbas  24030  fclsrest  24033  fclscf  24034  fclsfnflim  24036  flimfnfcls  24037  fclscmp  24039  ufilcmp  24041  isfcf  24043  fcfnei  24044  clssubg  24118  ustfilxp  24222  metustfbas  24571  restmetu  24584  reperflem  24841  metdseq0  24877  relcmpcmet  25353  bcthlem5  25363  minveclem4a  25465  dvlip  26033  wlkvtxiedg  29644  imadifxp  32615  constrextdg2lem  33790  bnj970  34962  neibastop1  36361  neibastop2  36363  heibor1lem  37817  isnumbasabl  43123  dfacbasgrp  43125  ioossioobi  45535  islptre  45639  stoweidlem35  46055  stoweidlem39  46059  fourierdlem46  46172
  Copyright terms: Public domain W3C validator