Theorem ssn0 4384

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2933   ⊆ wss 3931  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-dif 3934  df-ss 3948  df-nul 4314

This theorem is referenced by:  unixp0  6277  frxp  8130  onfununi  8360  frmin  9768  carddomi2  9989  fin23lem21  10358  wunex2  10757  vdwmc2  17004  gsumval2  18669  subgint  19138  subrngint  20525  subrgint  20560  nzerooringczr  21446  hausnei2  23296  fbun  23783  fbfinnfr  23784  filuni  23828  isufil2  23851  ufileu  23862  filufint  23863  fmfnfm  23901  hausflim  23924  flimclslem  23927  fclsneii  23960  fclsbas  23964  fclsrest  23967  fclscf  23968  fclsfnflim  23970  flimfnfcls  23971  fclscmp  23973  ufilcmp  23975  isfcf  23977  fcfnei  23978  clssubg  24052  ustfilxp  24156  metustfbas  24501  restmetu  24514  reperflem  24763  metdseq0  24799  relcmpcmet  25275  bcthlem5  25285  minveclem4a  25387  dvlip  25955  wlkvtxiedg  29610  imadifxp  32587  constrextdg2lem  33787  bnj970  34983  neibastop1  36382  neibastop2  36384  heibor1lem  37838  isnumbasabl  43097  dfacbasgrp  43099  ioossioobi  45513  islptre  45615  stoweidlem35  46031  stoweidlem39  46035  fourierdlem46  46148