Theorem ssn0 3691

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

Step	Hyp	Ref	Expression
1		sseq0 3690	. . . 4 |- ( ( A C_ B /\ B = (/) ) -> A = (/) )
2	1	ex 434	. . 3 |- ( A C_ B -> ( B = (/) -> A = (/) ) )
3	2	necon3d 2670	. 2 |- ( A C_ B -> ( A =/= (/) -> B =/= (/) ) )
4	3	imp 429	1 |- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   =/= wne 2620   C_ wss 3349   (/)c0 3658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-v 2995  df-dif 3352  df-in 3356  df-ss 3363  df-nul 3659

This theorem is referenced by:  unixp0  5392  frxp  6703  onfununi  6823  carddomi2  8161  fin23lem21  8529  wunex2  8926  vdwmc2  14061  gsumval2  15534  subgint  15726  subrgint  16909  hausnei2  18979  fbun  19435  fbfinnfr  19436  filuni  19480  isufil2  19503  ufileu  19514  filufint  19515  fmfnfm  19553  hausflim  19576  flimclslem  19579  fclsneii  19612  fclsbas  19616  fclsrest  19619  fclscf  19620  fclsfnflim  19622  flimfnfcls  19623  fclscmp  19625  ufilcmp  19627  isfcf  19629  fcfnei  19630  clssubg  19701  ustfilxp  19809  metustfbasOLD  20162  metustfbas  20163  restmetu  20184  reperflem  20417  metdseq0  20452  relcmpcmet  20849  bcthlem5  20861  minveclem4a  20939  dvlip  21487  imadifxp  25961  frmin  27725  neibastop1  28606  neibastop2  28608  heibor1lem  28734  isnumbasabl  29488  dfacbasgrp  29490  stoweidlem35  29856  stoweidlem39  29860  bnj970  32036