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

Theorem ssn0 3605
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 3604 . . . 4  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
21ex 424 . . 3  |-  ( A 
C_  B  ->  ( B  =  (/)  ->  A  =  (/) ) )
32necon3d 2590 . 2  |-  ( A 
C_  B  ->  ( A  =/=  (/)  ->  B  =/=  (/) ) )
43imp 419 1  |-  ( ( A  C_  B  /\  A  =/=  (/) )  ->  B  =/=  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    =/= wne 2552    C_ wss 3265   (/)c0 3573
This theorem is referenced by:  unixp0  5345  frxp  6394  onfununi  6541  carddomi2  7792  fin23lem21  8154  wunex2  8548  vdwmc2  13276  gsumval2  14712  subgint  14893  subrgint  15819  hausnei2  17341  fbun  17795  fbfinnfr  17796  filuni  17840  isufil2  17863  ufileu  17874  filufint  17875  fmfnfm  17913  hausflim  17936  flimclslem  17939  fclsneii  17972  fclsbas  17976  fclsrest  17979  fclscf  17980  fclsfnflim  17982  flimfnfcls  17983  fclscmp  17985  ufilcmp  17987  isfcf  17989  fcfnei  17990  clssubg  18061  ustfilxp  18165  metustfbas  18479  restmetu  18491  reperflem  18722  metdseq0  18757  relcmpcmet  19142  bcthlem5  19152  minveclem4a  19200  dvlip  19746  imadifxp  23883  frmin  25268  neibastop1  26081  neibastop2  26083  heibor1lem  26211  isnumbasabl  26942  dfacbasgrp  26944  stoweidlem35  27454  stoweidlem39  27458  bnj970  28658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-v 2903  df-dif 3268  df-in 3272  df-ss 3279  df-nul 3574
  Copyright terms: Public domain W3C validator