Theorem ssn0 4403

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ≠ wne 2939   ⊆ wss 3950  ∅c0 4332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-dif 3953  df-ss 3967  df-nul 4333

This theorem is referenced by:  unixp0  6302  frxp  8152  onfununi  8382  frmin  9790  carddomi2  10011  fin23lem21  10380  wunex2  10779  vdwmc2  17018  gsumval2  18700  subgint  19169  subrngint  20561  subrgint  20596  nzerooringczr  21492  hausnei2  23362  fbun  23849  fbfinnfr  23850  filuni  23894  isufil2  23917  ufileu  23928  filufint  23929  fmfnfm  23967  hausflim  23990  flimclslem  23993  fclsneii  24026  fclsbas  24030  fclsrest  24033  fclscf  24034  fclsfnflim  24036  flimfnfcls  24037  fclscmp  24039  ufilcmp  24041  isfcf  24043  fcfnei  24044  clssubg  24118  ustfilxp  24222  metustfbas  24571  restmetu  24584  reperflem  24841  metdseq0  24877  relcmpcmet  25353  bcthlem5  25363  minveclem4a  25465  dvlip  26033  wlkvtxiedg  29644  imadifxp  32615  constrextdg2lem  33790  bnj970  34962  neibastop1  36361  neibastop2  36363  heibor1lem  37817  isnumbasabl  43123  dfacbasgrp  43125  ioossioobi  45535  islptre  45639  stoweidlem35  46055  stoweidlem39  46059  fourierdlem46  46172