Theorem ssn0 4345

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ≠ wne 2933   ⊆ wss 3890  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3893  df-ss 3907  df-nul 4275

This theorem is referenced by:  unixp0  6241  frxp  8069  onfununi  8274  frmin  9664  carddomi2  9885  fin23lem21  10252  wunex2  10652  vdwmc2  16941  gsumval2  18645  subgint  19117  subrngint  20528  subrgint  20563  nzerooringczr  21470  hausnei2  23328  fbun  23815  fbfinnfr  23816  filuni  23860  isufil2  23883  ufileu  23894  filufint  23895  fmfnfm  23933  hausflim  23956  flimclslem  23959  fclsneii  23992  fclsbas  23996  fclsrest  23999  fclscf  24000  fclsfnflim  24002  flimfnfcls  24003  fclscmp  24005  ufilcmp  24007  isfcf  24009  fcfnei  24010  clssubg  24084  ustfilxp  24188  metustfbas  24532  restmetu  24545  reperflem  24794  metdseq0  24830  relcmpcmet  25295  bcthlem5  25305  minveclem4a  25407  dvlip  25970  wlkvtxiedg  29708  imadifxp  32686  constrextdg2lem  33908  bnj970  35105  neibastop1  36557  neibastop2  36559  dfttc4  36728  elttcirr  36729  heibor1lem  38144  isnumbasabl  43552  dfacbasgrp  43554  ioossioobi  45965  islptre  46067  stoweidlem35  46481  stoweidlem39  46485  fourierdlem46  46598