Theorem ssn0 3620

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 3619	. . . 4 |- ( ( A C_ B /\ B = (/) ) -> A = (/) )
2	1	ex 424	. . 3 |- ( A C_ B -> ( B = (/) -> A = (/) ) )
3	2	necon3d 2605	. 2 |- ( A C_ B -> ( A =/= (/) -> B =/= (/) ) )
4	3	imp 419	1 |- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   =/= wne 2567   C_ wss 3280   (/)c0 3588

This theorem is referenced by:  unixp0  5362  frxp  6415  onfununi  6562  carddomi2  7813  fin23lem21  8175  wunex2  8569  vdwmc2  13302  gsumval2  14738  subgint  14919  subrgint  15845  hausnei2  17371  fbun  17825  fbfinnfr  17826  filuni  17870  isufil2  17893  ufileu  17904  filufint  17905  fmfnfm  17943  hausflim  17966  flimclslem  17969  fclsneii  18002  fclsbas  18006  fclsrest  18009  fclscf  18010  fclsfnflim  18012  flimfnfcls  18013  fclscmp  18015  ufilcmp  18017  isfcf  18019  fcfnei  18020  clssubg  18091  ustfilxp  18195  metustfbasOLD  18548  metustfbas  18549  restmetu  18570  reperflem  18802  metdseq0  18837  relcmpcmet  19222  bcthlem5  19234  minveclem4a  19284  dvlip  19830  imadifxp  23991  frmin  25456  neibastop1  26278  neibastop2  26280  heibor1lem  26408  isnumbasabl  27139  dfacbasgrp  27141  stoweidlem35  27651  stoweidlem39  27655  bnj970  29024

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294  df-nul 3589