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

Theorem ssn0 3604
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 3603 . . . 4  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
21ex 424 . . 3  |-  ( A 
C_  B  ->  ( B  =  (/)  ->  A  =  (/) ) )
32necon3d 2589 . 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 2551    C_ wss 3264   (/)c0 3572
This theorem is referenced by:  unixp0  5344  frxp  6393  onfununi  6540  carddomi2  7791  fin23lem21  8153  wunex2  8547  vdwmc2  13275  gsumval2  14711  subgint  14892  subrgint  15818  hausnei2  17340  fbun  17794  fbfinnfr  17795  filuni  17839  isufil2  17862  ufileu  17873  filufint  17874  fmfnfm  17912  hausflim  17935  flimclslem  17938  fclsneii  17971  fclsbas  17975  fclsrest  17978  fclscf  17979  fclsfnflim  17981  flimfnfcls  17982  fclscmp  17984  ufilcmp  17986  isfcf  17988  fcfnei  17989  clssubg  18060  ustfilxp  18164  metustfbas  18478  restmetu  18490  reperflem  18721  metdseq0  18756  relcmpcmet  19141  bcthlem5  19151  minveclem4a  19199  dvlip  19745  imadifxp  23882  frmin  25267  neibastop1  26080  neibastop2  26082  heibor1lem  26210  isnumbasabl  26941  dfacbasgrp  26943  stoweidlem35  27453  stoweidlem39  27457  bnj970  28657
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 2369
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-v 2902  df-dif 3267  df-in 3271  df-ss 3278  df-nul 3573
  Copyright terms: Public domain W3C validator