Theorem ssn0 4355

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2956   ⊆ wss 3899  ∅c0 4279

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  unixp0  6279  frxp  8127  onfununi  8333  frmin  9737  carddomi2  10032  fin23lem21  10398  wunex2  10804  vdwmc2  17137  gsumval2  18855  subgint  19341  subrngint  20792  subrgint  20827  nzerooringczr  21766  hausnei2  23651  fbun  24139  fbfinnfr  24140  filuni  24184  isufil2  24207  ufileu  24218  filufint  24219  fmfnfm  24257  hausflim  24280  flimclslem  24283  fclsneii  24316  fclsbas  24320  fclsrest  24323  fclscf  24324  fclsfnflim  24326  flimfnfcls  24327  fclscmp  24329  ufilcmp  24331  isfcf  24333  fcfnei  24334  clssubg  24408  ustfilxp  24512  metustfbas  24856  restmetu  24869  reperflem  25118  metdseq0  25154  relcmpcmet  25619  bcthlem5  25629  minveclem4a  25731  dvlip  26293  wlkvtxiedg  30187  imadifxp  33177  constrextdg2lem  34362  bnj970  35560  neibastop1  37117  neibastop2  37119  dfttc4  37288  elttcirr  37289  heibor1lem  38711  isnumbasabl  44066  dfacbasgrp  44068  ioossioobi  46473  islptre  46575  stoweidlem35  46989  stoweidlem39  46993  fourierdlem46  47106