Theorem ssn0 4427

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ≠ wne 2946   ⊆ wss 3976  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-dif 3979  df-ss 3993  df-nul 4353

This theorem is referenced by:  unixp0  6314  frxp  8167  onfununi  8397  frmin  9818  carddomi2  10039  fin23lem21  10408  wunex2  10807  vdwmc2  17026  gsumval2  18724  subgint  19190  subrngint  20586  subrgint  20623  nzerooringczr  21514  hausnei2  23382  fbun  23869  fbfinnfr  23870  filuni  23914  isufil2  23937  ufileu  23948  filufint  23949  fmfnfm  23987  hausflim  24010  flimclslem  24013  fclsneii  24046  fclsbas  24050  fclsrest  24053  fclscf  24054  fclsfnflim  24056  flimfnfcls  24057  fclscmp  24059  ufilcmp  24061  isfcf  24063  fcfnei  24064  clssubg  24138  ustfilxp  24242  metustfbas  24591  restmetu  24604  reperflem  24859  metdseq0  24895  relcmpcmet  25371  bcthlem5  25381  minveclem4a  25483  dvlip  26052  wlkvtxiedg  29661  imadifxp  32623  bnj970  34923  neibastop1  36325  neibastop2  36327  heibor1lem  37769  isnumbasabl  43063  dfacbasgrp  43065  ioossioobi  45435  islptre  45540  stoweidlem35  45956  stoweidlem39  45960  fourierdlem46  46073