MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snss Structured version   Visualization version   GIF version

Theorem snss 4712
Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4711). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
snss.1 𝐴 ∈ V
Assertion
Ref Expression
snss (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵)

Proof of Theorem snss
StepHypRef Expression
1 snss.1 . 2 𝐴 ∈ V
2 snssg 4711 . 2 (𝐴 ∈ V → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
31, 2ax-mp 5 1 (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105  Vcvv 3495  wss 3935  {csn 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-in 3942  df-ss 3951  df-sn 4560
This theorem is referenced by:  tpss  4762  snelpw  5329  sspwb  5333  nnullss  5346  exss  5347  pwssun  5449  fvimacnvi  6815  fvimacnv  6816  fvimacnvALT  6820  fnressn  6913  limensuci  8682  domunfican  8780  finsschain  8820  epfrs  9162  tc2  9173  tcsni  9174  dju1dif  9587  fpwwe2lem13  10053  wunfi  10132  uniwun  10151  un0mulcl  11920  nn0ssz  11992  xrinfmss  12693  hashbclem  13800  hashf1lem1  13803  hashf1lem2  13804  fsum2dlem  15115  fsumabs  15146  fsumrlim  15156  fsumo1  15157  fsumiun  15166  incexclem  15181  fprod2dlem  15324  lcmfunsnlem  15975  lcmfun  15979  coprmprod  15995  coprmproddvdslem  15996  ramcl2  16342  0ram  16346  strfv  16521  imasaddfnlem  16791  imasaddvallem  16792  acsfn1  16922  drsdirfi  17538  sylow2a  18675  gsumpt  19013  dprdfadd  19073  ablfac1eulem  19125  pgpfaclem1  19134  acsfn1p  19509  rsp1  19927  mplcoe1  20176  mplcoe5  20179  mdetunilem9  21159  opnnei  21658  iscnp4  21801  cnpnei  21802  hausnei2  21891  fiuncmp  21942  llycmpkgen2  22088  1stckgen  22092  ptbasfi  22119  xkoccn  22157  xkoptsub  22192  ptcmpfi  22351  cnextcn  22605  tsmsid  22677  ustuqtop3  22781  utopreg  22790  prdsdsf  22906  prdsmet  22909  prdsbl  23030  fsumcn  23407  itgfsum  24356  dvmptfsum  24501  elply2  24715  elplyd  24721  ply1term  24723  ply0  24727  plymullem  24735  jensenlem1  25492  jensenlem2  25493  frcond3  27976  h1de2bi  29259  spansni  29262  gsumle  30653  gsumvsca1  30782  gsumvsca2  30783  extdg1id  30953  ordtconnlem1  31067  cntnevol  31387  eulerpartgbij  31530  breprexpnat  31805  cvmlift2lem1  32447  cvmlift2lem12  32459  dfon2lem7  32932  bj-tagss  34190  lindsenlbs  34769  matunitlindflem1  34770  divrngidl  35189  isfldidl  35229  ispridlc  35231  pclfinclN  36968  osumcllem10N  36983  pexmidlem7N  36994  clsk1indlem4  40274  clsk1indlem1  40275  fourierdlem62  42334
  Copyright terms: Public domain W3C validator