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

Theorem ssn0 4351
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 4350 . . . 4 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
21ex 413 . . 3 (𝐴𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
32necon3d 3034 . 2 (𝐴𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
43imp 407 1 ((𝐴𝐵𝐴 ≠ ∅) → 𝐵 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wne 3013  wss 3933  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ne 3014  df-dif 3936  df-in 3940  df-ss 3949  df-nul 4289
This theorem is referenced by:  unixp0  6127  frxp  7809  onfununi  7967  carddomi2  9387  fin23lem21  9749  wunex2  10148  vdwmc2  16303  gsumval2  17884  subgint  18241  subrgint  19486  hausnei2  21889  fbun  22376  fbfinnfr  22377  filuni  22421  isufil2  22444  ufileu  22455  filufint  22456  fmfnfm  22494  hausflim  22517  flimclslem  22520  fclsneii  22553  fclsbas  22557  fclsrest  22560  fclscf  22561  fclsfnflim  22563  flimfnfcls  22564  fclscmp  22566  ufilcmp  22568  isfcf  22570  fcfnei  22571  clssubg  22644  ustfilxp  22748  metustfbas  23094  restmetu  23107  reperflem  23353  metdseq0  23389  relcmpcmet  23848  bcthlem5  23858  minveclem4a  23960  dvlip  24517  wlkvtxiedg  27333  imadifxp  30279  bnj970  32118  frmin  32981  neibastop1  33604  neibastop2  33606  heibor1lem  34968  isnumbasabl  39584  dfacbasgrp  39586  ioossioobi  41669  islptre  41776  stoweidlem35  42197  stoweidlem39  42201  fourierdlem46  42314  nzerooringczr  44271
  Copyright terms: Public domain W3C validator