Theorem ssn0 3818

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 3817	. . . 4 |- ( ( A C_ B /\ B = (/) ) -> A = (/) )
2	1	ex 434	. . 3 |- ( A C_ B -> ( B = (/) -> A = (/) ) )
3	2	necon3d 2691	. 2 |- ( A C_ B -> ( A =/= (/) -> B =/= (/) ) )
4	3	imp 429	1 |- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   =/= wne 2662   C_ wss 3476   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786

This theorem is referenced by:  unixp0  5541  frxp  6893  onfununi  7012  carddomi2  8351  fin23lem21  8719  wunex2  9116  vdwmc2  14356  gsumval2  15835  subgint  16030  subrgint  17251  hausnei2  19648  fbun  20104  fbfinnfr  20105  filuni  20149  isufil2  20172  ufileu  20183  filufint  20184  fmfnfm  20222  hausflim  20245  flimclslem  20248  fclsneii  20281  fclsbas  20285  fclsrest  20288  fclscf  20289  fclsfnflim  20291  flimfnfcls  20292  fclscmp  20294  ufilcmp  20296  isfcf  20298  fcfnei  20299  clssubg  20370  ustfilxp  20478  metustfbasOLD  20831  metustfbas  20832  restmetu  20853  reperflem  21086  metdseq0  21121  relcmpcmet  21518  bcthlem5  21530  minveclem4a  21608  dvlip  22157  imadifxp  27159  frmin  28927  neibastop1  29808  neibastop2  29810  heibor1lem  29936  isnumbasabl  30687  dfacbasgrp  30689  ioossioobi  31149  islptre  31189  stoweidlem35  31363  stoweidlem39  31367  fourierdlem46  31481  bnj970  33102