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

Theorem snss 4751
Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4749). 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 4749 . 2 (𝐴 ∈ V → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
31, 2ax-mp 5 1 (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2107  Vcvv 3448  wss 3915  {csn 4591
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-sn 4592
This theorem is referenced by:  tpss  4800  sspwb  5411  nnullss  5424  exss  5425  pwssun  5533  fvimacnvi  7007  fvimacnv  7008  fvimacnvALT  7012  fnressn  7109  limensuci  9104  domunfican  9271  finsschain  9310  epfrs  9674  tc2  9685  tcsni  9686  dju1dif  10115  fpwwe2lem12  10585  wunfi  10664  uniwun  10683  un0mulcl  12454  nn0ssz  12529  xrinfmss  13236  hashbclem  14356  hashf1lem1  14360  hashf1lem1OLD  14361  hashf1lem2  14362  fsum2dlem  15662  fsumabs  15693  fsumrlim  15703  fsumo1  15704  fsumiun  15713  incexclem  15728  fprod2dlem  15870  lcmfunsnlem  16524  lcmfun  16528  coprmprod  16544  coprmproddvdslem  16545  ramcl2  16895  0ram  16899  strfv  17083  imasaddfnlem  17417  imasaddvallem  17418  acsfn1  17548  drsdirfi  18201  sylow2a  19408  gsumpt  19746  dprdfadd  19806  ablfac1eulem  19858  pgpfaclem1  19867  acsfn1p  20282  rsp1  20710  mplcoe1  21454  mplcoe5  21457  mdetunilem9  21985  opnnei  22487  iscnp4  22630  cnpnei  22631  hausnei2  22720  fiuncmp  22771  llycmpkgen2  22917  1stckgen  22921  ptbasfi  22948  xkoccn  22986  xkoptsub  23021  ptcmpfi  23180  cnextcn  23434  tsmsid  23507  ustuqtop3  23611  utopreg  23620  prdsdsf  23736  prdsmet  23739  prdsbl  23863  fsumcn  24249  itgfsum  25207  dvmptfsum  25355  elply2  25573  elplyd  25579  ply1term  25581  ply0  25585  plymullem  25593  jensenlem1  26352  jensenlem2  26353  frcond3  29255  h1de2bi  30538  spansni  30541  gsumle  31974  gsumvsca1  32103  gsumvsca2  32104  1fldgenq  32129  extdg1id  32392  ordtconnlem1  32545  cntnevol  32867  eulerpartgbij  33012  breprexpnat  33287  cvmlift2lem1  33936  cvmlift2lem12  33948  dfon2lem7  34403  bj-tagss  35480  lindsenlbs  36102  matunitlindflem1  36103  divrngidl  36516  isfldidl  36556  ispridlc  36558  pclfinclN  38442  osumcllem10N  38457  pexmidlem7N  38468  clsk1indlem4  42390  clsk1indlem1  42391  fourierdlem62  44483
  Copyright terms: Public domain W3C validator