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

Theorem ssn0 3928
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 3927 . . . 4 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
21ex 449 . . 3 (𝐴𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
32necon3d 2803 . 2 (𝐴𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
43imp 444 1 ((𝐴𝐵𝐴 ≠ ∅) → 𝐵 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wne 2780  wss 3540  c0 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875
This theorem is referenced by:  unixp0  5586  frxp  7174  onfununi  7325  carddomi2  8679  fin23lem21  9044  wunex2  9439  vdwmc2  15521  gsumval2  17103  subgint  17441  subrgint  18625  hausnei2  20967  fbun  21454  fbfinnfr  21455  filuni  21499  isufil2  21522  ufileu  21533  filufint  21534  fmfnfm  21572  hausflim  21595  flimclslem  21598  fclsneii  21631  fclsbas  21635  fclsrest  21638  fclscf  21639  fclsfnflim  21641  flimfnfcls  21642  fclscmp  21644  ufilcmp  21646  isfcf  21648  fcfnei  21649  clssubg  21722  ustfilxp  21826  metustfbas  22172  restmetu  22185  reperflem  22429  metdseq0  22465  relcmpcmet  22923  bcthlem5  22933  minveclem4a  23009  dvlip  23560  imadifxp  28796  bnj970  30271  frmin  30983  neibastop1  31524  neibastop2  31526  heibor1lem  32778  isnumbasabl  36695  dfacbasgrp  36697  ioossioobi  38590  islptre  38686  stoweidlem35  38928  stoweidlem39  38932  fourierdlem46  39045  1wlkvtxiedg  40829  nzerooringczr  41864
  Copyright terms: Public domain W3C validator