Theorem ssn0 4344

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ≠ wne 2932   ⊆ wss 3889  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3892  df-ss 3906  df-nul 4274

This theorem is referenced by:  unixp0  6247  frxp  8076  onfununi  8281  frmin  9673  carddomi2  9894  fin23lem21  10261  wunex2  10661  vdwmc2  16950  gsumval2  18654  subgint  19126  subrngint  20537  subrgint  20572  nzerooringczr  21460  hausnei2  23318  fbun  23805  fbfinnfr  23806  filuni  23850  isufil2  23873  ufileu  23884  filufint  23885  fmfnfm  23923  hausflim  23946  flimclslem  23949  fclsneii  23982  fclsbas  23986  fclsrest  23989  fclscf  23990  fclsfnflim  23992  flimfnfcls  23993  fclscmp  23995  ufilcmp  23997  isfcf  23999  fcfnei  24000  clssubg  24074  ustfilxp  24178  metustfbas  24522  restmetu  24535  reperflem  24784  metdseq0  24820  relcmpcmet  25285  bcthlem5  25295  minveclem4a  25397  dvlip  25960  wlkvtxiedg  29693  imadifxp  32671  constrextdg2lem  33892  bnj970  35089  neibastop1  36541  neibastop2  36543  dfttc4  36712  elttcirr  36713  heibor1lem  38130  isnumbasabl  43534  dfacbasgrp  43536  ioossioobi  45947  islptre  46049  stoweidlem35  46463  stoweidlem39  46467  fourierdlem46  46580