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

Theorem snss 4703
Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4702). 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 4702 . 2 (𝐴 ∈ V → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
31, 2ax-mp 5 1 (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wcel 2115  Vcvv 3480  wss 3919  {csn 4550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-sn 4551
This theorem is referenced by:  tpss  4752  snelpw  5325  sspwb  5329  nnullss  5341  exss  5342  pwssun  5443  fvimacnvi  6813  fvimacnv  6814  fvimacnvALT  6818  fnressn  6911  limensuci  8690  domunfican  8788  finsschain  8828  epfrs  9170  tc2  9181  tcsni  9182  dju1dif  9596  fpwwe2lem13  10062  wunfi  10141  uniwun  10160  un0mulcl  11928  nn0ssz  12000  xrinfmss  12700  hashbclem  13815  hashf1lem1  13818  hashf1lem2  13819  fsum2dlem  15125  fsumabs  15156  fsumrlim  15166  fsumo1  15167  fsumiun  15176  incexclem  15191  fprod2dlem  15334  lcmfunsnlem  15983  lcmfun  15987  coprmprod  16003  coprmproddvdslem  16004  ramcl2  16350  0ram  16354  strfv  16531  imasaddfnlem  16801  imasaddvallem  16802  acsfn1  16932  drsdirfi  17548  sylow2a  18744  gsumpt  19082  dprdfadd  19142  ablfac1eulem  19194  pgpfaclem1  19203  acsfn1p  19578  rsp1  19997  mplcoe1  20246  mplcoe5  20249  mdetunilem9  21229  opnnei  21728  iscnp4  21871  cnpnei  21872  hausnei2  21961  fiuncmp  22012  llycmpkgen2  22158  1stckgen  22162  ptbasfi  22189  xkoccn  22227  xkoptsub  22262  ptcmpfi  22421  cnextcn  22675  tsmsid  22748  ustuqtop3  22852  utopreg  22861  prdsdsf  22977  prdsmet  22980  prdsbl  23101  fsumcn  23478  itgfsum  24433  dvmptfsum  24581  elply2  24796  elplyd  24802  ply1term  24804  ply0  24808  plymullem  24816  jensenlem1  25575  jensenlem2  25576  frcond3  28057  h1de2bi  29340  spansni  29343  gsumle  30757  gsumvsca1  30886  gsumvsca2  30887  extdg1id  31113  ordtconnlem1  31224  cntnevol  31544  eulerpartgbij  31687  breprexpnat  31962  cvmlift2lem1  32606  cvmlift2lem12  32618  dfon2lem7  33091  bj-tagss  34360  lindsenlbs  34997  matunitlindflem1  34998  divrngidl  35411  isfldidl  35451  ispridlc  35453  pclfinclN  37191  osumcllem10N  37206  pexmidlem7N  37217  clsk1indlem4  40666  clsk1indlem1  40667  fourierdlem62  42736
  Copyright terms: Public domain W3C validator