Theorem ssn0 4315

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 4314	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 416	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2961	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 410	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ≠ wne 2940   ⊆ wss 3866  ∅c0 4237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3410  df-dif 3869  df-in 3873  df-ss 3883  df-nul 4238

This theorem is referenced by:  unixp0  6146  frxp  7893  onfununi  8078  frmin  9365  carddomi2  9586  fin23lem21  9953  wunex2  10352  vdwmc2  16532  gsumval2  18158  subgint  18567  subrgint  19822  hausnei2  22250  fbun  22737  fbfinnfr  22738  filuni  22782  isufil2  22805  ufileu  22816  filufint  22817  fmfnfm  22855  hausflim  22878  flimclslem  22881  fclsneii  22914  fclsbas  22918  fclsrest  22921  fclscf  22922  fclsfnflim  22924  flimfnfcls  22925  fclscmp  22927  ufilcmp  22929  isfcf  22931  fcfnei  22932  clssubg  23006  ustfilxp  23110  metustfbas  23455  restmetu  23468  reperflem  23715  metdseq0  23751  relcmpcmet  24215  bcthlem5  24225  minveclem4a  24327  dvlip  24890  wlkvtxiedg  27712  imadifxp  30659  bnj970  32640  neibastop1  34285  neibastop2  34287  heibor1lem  35704  isnumbasabl  40634  dfacbasgrp  40636  ioossioobi  42730  islptre  42835  stoweidlem35  43251  stoweidlem39  43255  fourierdlem46  43368  nzerooringczr  45303