Theorem ssn0 4009

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 4008	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 449	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2844	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 444	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ≠ wne 2823   ⊆ wss 3607  ∅c0 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949

This theorem is referenced by:  unixp0  5707  frxp  7332  onfununi  7483  carddomi2  8834  fin23lem21  9199  wunex2  9598  vdwmc2  15730  gsumval2  17327  subgint  17665  subrgint  18850  hausnei2  21205  fbun  21691  fbfinnfr  21692  filuni  21736  isufil2  21759  ufileu  21770  filufint  21771  fmfnfm  21809  hausflim  21832  flimclslem  21835  fclsneii  21868  fclsbas  21872  fclsrest  21875  fclscf  21876  fclsfnflim  21878  flimfnfcls  21879  fclscmp  21881  ufilcmp  21883  isfcf  21885  fcfnei  21886  clssubg  21959  ustfilxp  22063  metustfbas  22409  restmetu  22422  reperflem  22668  metdseq0  22704  relcmpcmet  23161  bcthlem5  23171  minveclem4a  23247  dvlip  23801  wlkvtxiedg  26576  imadifxp  29540  bnj970  31143  frmin  31867  neibastop1  32479  neibastop2  32481  heibor1lem  33738  isnumbasabl  37993  dfacbasgrp  37995  ioossioobi  40061  islptre  40169  stoweidlem35  40570  stoweidlem39  40574  fourierdlem46  40687  nzerooringczr  42397