Theorem ssn0 4401

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ≠ wne 2941   ⊆ wss 3949  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  unixp0  6283  frxp  8112  onfununi  8341  frmin  9744  carddomi2  9965  fin23lem21  10334  wunex2  10733  vdwmc2  16912  gsumval2  18605  subgint  19030  subrgint  20342  hausnei2  22857  fbun  23344  fbfinnfr  23345  filuni  23389  isufil2  23412  ufileu  23423  filufint  23424  fmfnfm  23462  hausflim  23485  flimclslem  23488  fclsneii  23521  fclsbas  23525  fclsrest  23528  fclscf  23529  fclsfnflim  23531  flimfnfcls  23532  fclscmp  23534  ufilcmp  23536  isfcf  23538  fcfnei  23539  clssubg  23613  ustfilxp  23717  metustfbas  24066  restmetu  24079  reperflem  24334  metdseq0  24370  relcmpcmet  24835  bcthlem5  24845  minveclem4a  24947  dvlip  25510  wlkvtxiedg  28882  imadifxp  31832  bnj970  33958  neibastop1  35244  neibastop2  35246  heibor1lem  36677  isnumbasabl  41848  dfacbasgrp  41850  ioossioobi  44230  islptre  44335  stoweidlem35  44751  stoweidlem39  44755  fourierdlem46  44868  subrngint  46739  nzerooringczr  46970