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

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

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