Theorem ssn0 4280

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525   ≠ wne 2986   ⊆ wss 3865  ∅c0 4217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-ne 2987  df-dif 3868  df-in 3872  df-ss 3880  df-nul 4218

This theorem is referenced by:  unixp0  6016  frxp  7680  onfununi  7837  carddomi2  9252  fin23lem21  9614  wunex2  10013  vdwmc2  16148  gsumval2  17723  subgint  18061  subrgint  19251  hausnei2  21649  fbun  22136  fbfinnfr  22137  filuni  22181  isufil2  22204  ufileu  22215  filufint  22216  fmfnfm  22254  hausflim  22277  flimclslem  22280  fclsneii  22313  fclsbas  22317  fclsrest  22320  fclscf  22321  fclsfnflim  22323  flimfnfcls  22324  fclscmp  22326  ufilcmp  22328  isfcf  22330  fcfnei  22331  clssubg  22404  ustfilxp  22508  metustfbas  22854  restmetu  22867  reperflem  23113  metdseq0  23149  relcmpcmet  23608  bcthlem5  23618  minveclem4a  23720  dvlip  24277  wlkvtxiedg  27093  imadifxp  30037  bnj970  31831  frmin  32695  neibastop1  33318  neibastop2  33320  heibor1lem  34640  isnumbasabl  39212  dfacbasgrp  39214  ioossioobi  41356  islptre  41463  stoweidlem35  41884  stoweidlem39  41888  fourierdlem46  42001  nzerooringczr  43843