Theorem ssn0 4365

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2961   ⊆ wss 3908  ∅c0 4289

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-dif 3911  df-ss 3925  df-nul 4290

This theorem is used by:  unixp0  6291  frxp  8131  onfununi  8337  frmin  9731  carddomi2  9975  fin23lem21  10341  wunex2  10741  vdwmc2  17064  gsumval2  18773  subgint  19248  subrngint  20696  subrgint  20731  nzerooringczr  21667  hausnei2  23547  fbun  24034  fbfinnfr  24035  filuni  24079  isufil2  24102  ufileu  24113  filufint  24114  fmfnfm  24152  hausflim  24175  flimclslem  24178  fclsneii  24211  fclsbas  24215  fclsrest  24218  fclscf  24219  fclsfnflim  24221  flimfnfcls  24222  fclscmp  24224  ufilcmp  24226  isfcf  24228  fcfnei  24229  clssubg  24303  ustfilxp  24407  metustfbas  24751  restmetu  24764  reperflem  25013  metdseq0  25049  relcmpcmet  25514  bcthlem5  25524  minveclem4a  25626  dvlip  26189  wlkvtxiedg  30011  imadifxp  32983  constrextdg2lem  34169  bnj970  35367  neibastop1  36911  neibastop2  36913  dfttc4  37082  elttcirr  37083  heibor1lem  38501  isnumbasabl  43874  dfacbasgrp  43876  ioossioobi  46274  islptre  46376  stoweidlem35  46790  stoweidlem39  46794  fourierdlem46  46907