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

Theorem snss 4506
Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4505). 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 4505 . 2 (𝐴 ∈ V → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
31, 2ax-mp 5 1 (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wcel 2156  Vcvv 3391  wss 3769  {csn 4370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-ss 3783  df-sn 4371
This theorem is referenced by:  snssgOLD  4507  tpss  4556  snelpw  5103  sspwb  5107  nnullss  5120  exss  5121  pwssun  5215  relsnOLD  5428  fvimacnvi  6553  fvimacnv  6554  fvimacnvALT  6558  fnressn  6649  limensuci  8375  domunfican  8472  finsschain  8512  epfrs  8854  tc2  8865  tcsni  8866  cda1dif  9283  fpwwe2lem13  9749  wunfi  9828  uniwun  9847  un0mulcl  11593  nn0ssz  11664  xrinfmss  12358  hashbclem  13453  hashf1lem1  13456  hashf1lem2  13457  fsum2dlem  14724  fsumabs  14755  fsumrlim  14765  fsumo1  14766  fsumiun  14775  incexclem  14790  fprod2dlem  14931  lcmfunsnlem  15573  lcmfun  15577  coprmprod  15593  coprmproddvdslem  15594  ramcl2  15937  0ram  15941  strfv  16118  imasaddfnlem  16393  imasaddvallem  16394  acsfn1  16526  drsdirfi  17143  sylow2a  18235  gsumpt  18562  dprdfadd  18621  ablfac1eulem  18673  pgpfaclem1  18682  rsp1  19433  mplcoe1  19674  mplcoe5  19677  mdetunilem9  20637  opnnei  21138  iscnp4  21281  cnpnei  21282  hausnei2  21371  fiuncmp  21421  llycmpkgen2  21567  1stckgen  21571  ptbasfi  21598  xkoccn  21636  xkoptsub  21671  ptcmpfi  21830  cnextcn  22084  tsmsid  22156  ustuqtop3  22260  utopreg  22269  prdsdsf  22385  prdsmet  22388  prdsbl  22509  fsumcn  22886  itgfsum  23807  dvmptfsum  23952  elply2  24166  elplyd  24172  ply1term  24174  ply0  24178  plymullem  24186  jensenlem1  24927  jensenlem2  24928  frcond3  27444  h1de2bi  28741  spansni  28744  gsumle  30104  gsumvsca1  30107  gsumvsca2  30108  ordtconnlem1  30295  cntnevol  30616  eulerpartgbij  30759  breprexpnat  31037  cvmlift2lem1  31607  cvmlift2lem12  31619  dfon2lem7  32014  bj-tagss  33278  lindsenlbs  33717  matunitlindflem1  33718  divrngidl  34138  isfldidl  34178  ispridlc  34180  pclfinclN  35730  osumcllem10N  35745  pexmidlem7N  35756  acsfn1p  38270  clsk1indlem4  38842  clsk1indlem1  38843  fourierdlem62  40864
  Copyright terms: Public domain W3C validator