Theorem ssn0 4367

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3914  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-dif 3917  df-ss 3931  df-nul 4297

This theorem is referenced by:  unixp0  6256  frxp  8105  onfununi  8310  frmin  9702  carddomi2  9923  fin23lem21  10292  wunex2  10691  vdwmc2  16950  gsumval2  18613  subgint  19082  subrngint  20469  subrgint  20504  nzerooringczr  21390  hausnei2  23240  fbun  23727  fbfinnfr  23728  filuni  23772  isufil2  23795  ufileu  23806  filufint  23807  fmfnfm  23845  hausflim  23868  flimclslem  23871  fclsneii  23904  fclsbas  23908  fclsrest  23911  fclscf  23912  fclsfnflim  23914  flimfnfcls  23915  fclscmp  23917  ufilcmp  23919  isfcf  23921  fcfnei  23922  clssubg  23996  ustfilxp  24100  metustfbas  24445  restmetu  24458  reperflem  24707  metdseq0  24743  relcmpcmet  25218  bcthlem5  25228  minveclem4a  25330  dvlip  25898  wlkvtxiedg  29553  imadifxp  32530  constrextdg2lem  33738  bnj970  34937  neibastop1  36347  neibastop2  36349  heibor1lem  37803  isnumbasabl  43095  dfacbasgrp  43097  ioossioobi  45515  islptre  45617  stoweidlem35  46033  stoweidlem39  46037  fourierdlem46  46150