Theorem ssn0 4410

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 4409	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 412	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2959	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ≠ wne 2938   ⊆ wss 3963  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-dif 3966  df-ss 3980  df-nul 4340

This theorem is referenced by:  unixp0  6305  frxp  8150  onfununi  8380  frmin  9787  carddomi2  10008  fin23lem21  10377  wunex2  10776  vdwmc2  17013  gsumval2  18712  subgint  19181  subrngint  20577  subrgint  20612  nzerooringczr  21509  hausnei2  23377  fbun  23864  fbfinnfr  23865  filuni  23909  isufil2  23932  ufileu  23943  filufint  23944  fmfnfm  23982  hausflim  24005  flimclslem  24008  fclsneii  24041  fclsbas  24045  fclsrest  24048  fclscf  24049  fclsfnflim  24051  flimfnfcls  24052  fclscmp  24054  ufilcmp  24056  isfcf  24058  fcfnei  24059  clssubg  24133  ustfilxp  24237  metustfbas  24586  restmetu  24599  reperflem  24854  metdseq0  24890  relcmpcmet  25366  bcthlem5  25376  minveclem4a  25478  dvlip  26047  wlkvtxiedg  29658  imadifxp  32621  bnj970  34940  neibastop1  36342  neibastop2  36344  heibor1lem  37796  isnumbasabl  43095  dfacbasgrp  43097  ioossioobi  45470  islptre  45575  stoweidlem35  45991  stoweidlem39  45995  fourierdlem46  46108