Theorem ssn0 4339

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 4338	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 413	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2956	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ≠ wne 2935   ⊆ wss 3890  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-dif 3893  df-ss 3907  df-nul 4269

This theorem is referenced by:  unixp0  6241  frxp  8073  onfununi  8278  frmin  9671  carddomi2  9892  fin23lem21  10259  wunex2  10659  vdwmc2  16948  gsumval2  18652  subgint  19124  subrngint  20539  subrgint  20574  nzerooringczr  21462  hausnei2  23343  fbun  23830  fbfinnfr  23831  filuni  23875  isufil2  23898  ufileu  23909  filufint  23910  fmfnfm  23948  hausflim  23971  flimclslem  23974  fclsneii  24007  fclsbas  24011  fclsrest  24014  fclscf  24015  fclsfnflim  24017  flimfnfcls  24018  fclscmp  24020  ufilcmp  24022  isfcf  24024  fcfnei  24025  clssubg  24099  ustfilxp  24203  metustfbas  24547  restmetu  24560  reperflem  24809  metdseq0  24845  relcmpcmet  25310  bcthlem5  25320  minveclem4a  25422  dvlip  25985  wlkvtxiedg  29718  imadifxp  32697  constrextdg2lem  33939  bnj970  35136  neibastop1  36594  neibastop2  36596  dfttc4  36765  elttcirr  36766  heibor1lem  38183  isnumbasabl  43558  dfacbasgrp  43560  ioossioobi  45969  islptre  46071  stoweidlem35  46485  stoweidlem39  46489  fourierdlem46  46602