Theorem ssn0 4345

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 4344	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 413	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2962	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ≠ wne 2941   ⊆ wss 3897  ∅c0 4267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-v 3443  df-dif 3900  df-in 3904  df-ss 3914  df-nul 4268

This theorem is referenced by:  unixp0  6208  frxp  8011  onfununi  8219  frmin  9578  carddomi2  9799  fin23lem21  10168  wunex2  10567  vdwmc2  16750  gsumval2  18440  subgint  18848  subrgint  20118  hausnei2  22576  fbun  23063  fbfinnfr  23064  filuni  23108  isufil2  23131  ufileu  23142  filufint  23143  fmfnfm  23181  hausflim  23204  flimclslem  23207  fclsneii  23240  fclsbas  23244  fclsrest  23247  fclscf  23248  fclsfnflim  23250  flimfnfcls  23251  fclscmp  23253  ufilcmp  23255  isfcf  23257  fcfnei  23258  clssubg  23332  ustfilxp  23436  metustfbas  23785  restmetu  23798  reperflem  24053  metdseq0  24089  relcmpcmet  24554  bcthlem5  24564  minveclem4a  24666  dvlip  25229  wlkvtxiedg  28101  imadifxp  31048  bnj970  33032  neibastop1  34606  neibastop2  34608  heibor1lem  36023  isnumbasabl  41135  dfacbasgrp  41137  ioossioobi  43292  islptre  43397  stoweidlem35  43813  stoweidlem39  43817  fourierdlem46  43930  nzerooringczr  45882