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

Step	Hyp	Ref	Expression
1		sseq0 3778	. . . 4 |- ( ( A C_ B /\ B = (/) ) -> A = (/) )
2	1	ex 440	. . 3 |- ( A C_ B -> ( B = (/) -> A = (/) ) )
3	2	necon3d 2657	. 2 |- ( A C_ B -> ( A =/= (/) -> B =/= (/) ) )
4	3	imp 435	1 |- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )

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