Theorem ssn0 4119

Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)

Assertion

Ref	Expression
ssn0	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Proof of Theorem ssn0

Step	Hyp	Ref	Expression
1		sseq0 4118	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 449	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2953	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 444	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ≠ wne 2932   ⊆ wss 3715  ∅c0 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-v 3342  df-dif 3718  df-in 3722  df-ss 3729  df-nul 4059

This theorem is referenced by:  unixp0  5830  frxp  7455  onfununi  7607  carddomi2  8986  fin23lem21  9353  wunex2  9752  vdwmc2  15885  gsumval2  17481  subgint  17819  subrgint  19004  hausnei2  21359  fbun  21845  fbfinnfr  21846  filuni  21890  isufil2  21913  ufileu  21924  filufint  21925  fmfnfm  21963  hausflim  21986  flimclslem  21989  fclsneii  22022  fclsbas  22026  fclsrest  22029  fclscf  22030  fclsfnflim  22032  flimfnfcls  22033  fclscmp  22035  ufilcmp  22037  isfcf  22039  fcfnei  22040  clssubg  22113  ustfilxp  22217  metustfbas  22563  restmetu  22576  reperflem  22822  metdseq0  22858  relcmpcmet  23315  bcthlem5  23325  minveclem4a  23401  dvlip  23955  wlkvtxiedg  26730  imadifxp  29721  bnj970  31324  frmin  32048  neibastop1  32660  neibastop2  32662  heibor1lem  33921  isnumbasabl  38178  dfacbasgrp  38180  ioossioobi  40246  islptre  40354  stoweidlem35  40755  stoweidlem39  40759  fourierdlem46  40872  nzerooringczr  42582