Theorem ssn0 3976

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 3975	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
2	1	ex 450	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅))
3	2	necon3d 2815	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅))
4	3	imp 445	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ≠ wne 2794   ⊆ wss 3574  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  unixp0  5669  frxp  7287  onfununi  7438  carddomi2  8796  fin23lem21  9161  wunex2  9560  vdwmc2  15683  gsumval2  17280  subgint  17618  subrgint  18802  hausnei2  21157  fbun  21644  fbfinnfr  21645  filuni  21689  isufil2  21712  ufileu  21723  filufint  21724  fmfnfm  21762  hausflim  21785  flimclslem  21788  fclsneii  21821  fclsbas  21825  fclsrest  21828  fclscf  21829  fclsfnflim  21831  flimfnfcls  21832  fclscmp  21834  ufilcmp  21836  isfcf  21838  fcfnei  21839  clssubg  21912  ustfilxp  22016  metustfbas  22362  restmetu  22375  reperflem  22621  metdseq0  22657  relcmpcmet  23115  bcthlem5  23125  minveclem4a  23201  dvlip  23756  wlkvtxiedg  26520  imadifxp  29414  bnj970  31017  frmin  31739  neibastop1  32354  neibastop2  32356  heibor1lem  33608  isnumbasabl  37676  dfacbasgrp  37678  ioossioobi  39743  islptre  39851  stoweidlem35  40252  stoweidlem39  40256  fourierdlem46  40369  nzerooringczr  42072