Theorem ssn0 3927

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 3926	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 448	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2802	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 443	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1474   ≠ wne 2779   ⊆ wss 3539  ∅c0 3873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-v 3174  df-dif 3542  df-in 3546  df-ss 3553  df-nul 3874

This theorem is referenced by:  unixp0  5572  frxp  7152  onfununi  7303  carddomi2  8657  fin23lem21  9022  wunex2  9417  vdwmc2  15470  gsumval2  17052  subgint  17390  subrgint  18574  hausnei2  20915  fbun  21402  fbfinnfr  21403  filuni  21447  isufil2  21470  ufileu  21481  filufint  21482  fmfnfm  21520  hausflim  21543  flimclslem  21546  fclsneii  21579  fclsbas  21583  fclsrest  21586  fclscf  21587  fclsfnflim  21589  flimfnfcls  21590  fclscmp  21592  ufilcmp  21594  isfcf  21596  fcfnei  21597  clssubg  21670  ustfilxp  21774  metustfbas  22120  restmetu  22133  reperflem  22377  metdseq0  22413  relcmpcmet  22868  bcthlem5  22878  minveclem4a  22954  dvlip  23505  imadifxp  28630  bnj970  30105  frmin  30817  neibastop1  31358  neibastop2  31360  heibor1lem  32602  isnumbasabl  36519  dfacbasgrp  36521  ioossioobi  38414  islptre  38510  stoweidlem35  38752  stoweidlem39  38756  fourierdlem46  38869  1wlkvtxiedg  40851  nzerooringczr  41886