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

Theorem ssn0 3487
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 3486 . . . 4  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
21ex 423 . . 3  |-  ( A 
C_  B  ->  ( B  =  (/)  ->  A  =  (/) ) )
32necon3d 2484 . 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 1623    =/= wne 2446    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  unixp0  5206  frxp  6225  onfununi  6358  carddomi2  7603  fin23lem21  7965  wunex2  8360  vdwmc2  13026  gsumval2  14460  subgint  14641  subrgint  15567  hausnei2  17081  fbun  17535  fbfinnfr  17536  filuni  17580  isufil2  17603  ufileu  17614  filufint  17615  fmfnfm  17653  hausflim  17676  flimclslem  17679  fclsneii  17712  fclsbas  17716  fclsrest  17719  fclscf  17720  fclsfnflim  17722  flimfnfcls  17723  fclscmp  17725  ufilcmp  17727  isfcf  17729  fcfnei  17730  clssubg  17791  reperflem  18323  metdseq0  18358  relcmpcmet  18742  bcthlem5  18750  minveclem4a  18794  dvlip  19340  frmin  24242  cnfilca  25556  neibastop1  26308  neibastop2  26310  heibor1lem  26533  isnumbasabl  27271  dfacbasgrp  27273  stoweidlem35  27784  stoweidlem39  27788  bnj970  28979
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator