Theorem snss 4789

Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4787). 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

Step	Hyp	Ref	Expression
1		snss.1	. 2 ⊢ 𝐴 ∈ V
2		snssg 4787	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-sn 4631

This theorem is referenced by:  tpss  4841  sspwb  5459  nnullss  5472  exss  5473  pwssun  5579  fvimacnvi  7071  fvimacnv  7072  fvimacnvALT  7076  fnressn  7177  limensuci  9191  domunfican  9358  finsschain  9396  epfrs  9768  tc2  9779  tcsni  9780  dju1dif  10210  fpwwe2lem12  10679  wunfi  10758  uniwun  10777  un0mulcl  12557  nn0ssz  12633  xrinfmss  13348  hashbclem  14487  hashf1lem1  14490  hashf1lem2  14491  fsum2dlem  15802  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  incexclem  15868  fprod2dlem  16012  lcmfunsnlem  16674  lcmfun  16678  coprmprod  16694  coprmproddvdslem  16695  ramcl2  17049  0ram  17053  strfv  17237  imasaddfnlem  17574  imasaddvallem  17575  acsfn1  17705  drsdirfi  18362  sylow2a  19651  gsumpt  19994  dprdfadd  20054  ablfac1eulem  20106  pgpfaclem1  20115  acsfn1p  20816  rsp1  21264  pzriprnglem4  21512  mplcoe1  22072  mplcoe5  22075  mdetunilem9  22641  opnnei  23143  iscnp4  23286  cnpnei  23287  hausnei2  23376  fiuncmp  23427  llycmpkgen2  23573  1stckgen  23577  ptbasfi  23604  xkoccn  23642  xkoptsub  23677  ptcmpfi  23836  cnextcn  24090  tsmsid  24163  ustuqtop3  24267  utopreg  24276  prdsdsf  24392  prdsmet  24395  prdsbl  24519  fsumcn  24907  itgfsum  25876  dvmptfsum  26027  elply2  26249  elplyd  26255  ply1term  26257  ply0  26261  plymullem  26269  jensenlem1  27044  jensenlem2  27045  frcond3  30297  h1de2bi  31582  spansni  31585  gsumle  33083  gsumvsca1  33214  gsumvsca2  33215  1fldgenq  33303  unitprodclb  33396  mxidlirredi  33478  extdg1id  33690  ordtconnlem1  33884  cntnevol  34208  eulerpartgbij  34353  breprexpnat  34627  cvmlift2lem1  35286  cvmlift2lem12  35298  dfon2lem7  35770  bj-tagss  36962  lindsenlbs  37601  matunitlindflem1  37602  divrngidl  38014  isfldidl  38054  ispridlc  38056  pclfinclN  39932  osumcllem10N  39947  pexmidlem7N  39958  readvrec  42370  clsk1indlem4  44033  clsk1indlem1  44034  fourierdlem62  46123