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

Theorem ssn0 3779
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 3778 . . . 4  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
21ex 440 . . 3  |-  ( A 
C_  B  ->  ( B  =  (/)  ->  A  =  (/) ) )
32necon3d 2657 . 2  |-  ( A 
C_  B  ->  ( A  =/=  (/)  ->  B  =/=  (/) ) )
43imp 435 1  |-  ( ( A  C_  B  /\  A  =/=  (/) )  ->  B  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    =/= wne 2633    C_ wss 3416   (/)c0 3743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-v 3059  df-dif 3419  df-in 3423  df-ss 3430  df-nul 3744
This theorem is referenced by:  unixp0  5389  frxp  6933  onfununi  7086  carddomi2  8430  fin23lem21  8795  wunex2  9189  vdwmc2  14978  gsumval2  16572  subgint  16890  subrgint  18079  hausnei2  20418  fbun  20904  fbfinnfr  20905  filuni  20949  isufil2  20972  ufileu  20983  filufint  20984  fmfnfm  21022  hausflim  21045  flimclslem  21048  fclsneii  21081  fclsbas  21085  fclsrest  21088  fclscf  21089  fclsfnflim  21091  flimfnfcls  21092  fclscmp  21094  ufilcmp  21096  isfcf  21098  fcfnei  21099  clssubg  21172  ustfilxp  21276  metustfbas  21621  restmetu  21634  reperflem  21885  metdseq0  21920  metdseq0OLD  21935  relcmpcmet  22335  bcthlem5  22345  minveclem4a  22421  minveclem4aOLD  22433  dvlip  22994  imadifxp  28261  bnj970  29807  frmin  30529  neibastop1  31064  neibastop2  31066  heibor1lem  32186  isnumbasabl  36010  dfacbasgrp  36012  ioossioobi  37656  islptre  37737  stoweidlem35  37934  stoweidlem39  37938  fourierdlem46  38054  1wlkvtxiedg  39687  nzerooringczr  40347
  Copyright terms: Public domain W3C validator