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

Theorem ssn0 3500
Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
ssn0  |-  ( ( A  C_  B  /\  A  =/=  (/) )  ->  B  =/=  (/) )

Proof of Theorem ssn0
StepHypRef Expression
1 sseq0 3499 . . . 4  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
21ex 423 . . 3  |-  ( A 
C_  B  ->  ( B  =  (/)  ->  A  =  (/) ) )
32necon3d 2497 . 2  |-  ( A 
C_  B  ->  ( A  =/=  (/)  ->  B  =/=  (/) ) )
43imp 418 1  |-  ( ( A  C_  B  /\  A  =/=  (/) )  ->  B  =/=  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    =/= wne 2459    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  unixp0  5222  frxp  6241  onfununi  6374  carddomi2  7619  fin23lem21  7981  wunex2  8376  vdwmc2  13042  gsumval2  14476  subgint  14657  subrgint  15583  hausnei2  17097  fbun  17551  fbfinnfr  17552  filuni  17596  isufil2  17619  ufileu  17630  filufint  17631  fmfnfm  17669  hausflim  17692  flimclslem  17695  fclsneii  17728  fclsbas  17732  fclsrest  17735  fclscf  17736  fclsfnflim  17738  flimfnfcls  17739  fclscmp  17741  ufilcmp  17743  isfcf  17745  fcfnei  17746  clssubg  17807  reperflem  18339  metdseq0  18374  relcmpcmet  18758  bcthlem5  18766  minveclem4a  18810  dvlip  19356  frmin  24312  cnfilca  25658  neibastop1  26410  neibastop2  26412  heibor1lem  26635  isnumbasabl  27373  dfacbasgrp  27375  stoweidlem35  27886  stoweidlem39  27890  bnj970  29294
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator