Theorem ssn0 3827

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1395   =/= wne 2652   C_ wss 3471   (/)c0 3793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3794

This theorem is referenced by:  unixp0  5547  frxp  6909  onfununi  7030  carddomi2  8368  fin23lem21  8736  wunex2  9133  vdwmc2  14509  gsumval2  16034  subgint  16352  subrgint  17578  hausnei2  19981  fbun  20467  fbfinnfr  20468  filuni  20512  isufil2  20535  ufileu  20546  filufint  20547  fmfnfm  20585  hausflim  20608  flimclslem  20611  fclsneii  20644  fclsbas  20648  fclsrest  20651  fclscf  20652  fclsfnflim  20654  flimfnfcls  20655  fclscmp  20657  ufilcmp  20659  isfcf  20661  fcfnei  20662  clssubg  20733  ustfilxp  20841  metustfbasOLD  21194  metustfbas  21195  restmetu  21216  reperflem  21449  metdseq0  21484  relcmpcmet  21881  bcthlem5  21893  minveclem4a  21971  dvlip  22520  imadifxp  27600  frmin  29539  neibastop1  30382  neibastop2  30384  heibor1lem  30510  isnumbasabl  31259  dfacbasgrp  31261  ioossioobi  31760  islptre  31828  stoweidlem35  32020  stoweidlem39  32024  fourierdlem46  32138  nzerooringczr  33024  bnj970  34148