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

Theorem ssn0 3658
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 3657 . . . 4  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
21ex 434 . . 3  |-  ( A 
C_  B  ->  ( B  =  (/)  ->  A  =  (/) ) )
32necon3d 2636 . 2  |-  ( A 
C_  B  ->  ( A  =/=  (/)  ->  B  =/=  (/) ) )
43imp 429 1  |-  ( ( A  C_  B  /\  A  =/=  (/) )  ->  B  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    =/= wne 2596    C_ wss 3316   (/)c0 3625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-in 3323  df-ss 3330  df-nul 3626
This theorem is referenced by:  unixp0  5359  frxp  6671  onfununi  6788  carddomi2  8128  fin23lem21  8496  wunex2  8892  vdwmc2  14022  gsumval2  15492  subgint  15684  subrgint  16810  hausnei2  18798  fbun  19254  fbfinnfr  19255  filuni  19299  isufil2  19322  ufileu  19333  filufint  19334  fmfnfm  19372  hausflim  19395  flimclslem  19398  fclsneii  19431  fclsbas  19435  fclsrest  19438  fclscf  19439  fclsfnflim  19441  flimfnfcls  19442  fclscmp  19444  ufilcmp  19446  isfcf  19448  fcfnei  19449  clssubg  19520  ustfilxp  19628  metustfbasOLD  19981  metustfbas  19982  restmetu  20003  reperflem  20236  metdseq0  20271  relcmpcmet  20668  bcthlem5  20680  minveclem4a  20758  dvlip  21306  imadifxp  25762  frmin  27549  neibastop1  28421  neibastop2  28423  heibor1lem  28549  isnumbasabl  29304  dfacbasgrp  29306  stoweidlem35  29673  stoweidlem39  29677  bnj970  31639
  Copyright terms: Public domain W3C validator