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 205   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3948  {csn 4628

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-sn 4629

This theorem is referenced by:  tpss  4838  sspwb  5449  nnullss  5462  exss  5463  pwssun  5571  fvimacnvi  7053  fvimacnv  7054  fvimacnvALT  7058  fnressn  7155  limensuci  9152  domunfican  9319  finsschain  9358  epfrs  9725  tc2  9736  tcsni  9737  dju1dif  10166  fpwwe2lem12  10636  wunfi  10715  uniwun  10734  un0mulcl  12505  nn0ssz  12580  xrinfmss  13288  hashbclem  14410  hashf1lem1  14414  hashf1lem1OLD  14415  hashf1lem2  14416  fsum2dlem  15715  fsumabs  15746  fsumrlim  15756  fsumo1  15757  fsumiun  15766  incexclem  15781  fprod2dlem  15923  lcmfunsnlem  16577  lcmfun  16581  coprmprod  16597  coprmproddvdslem  16598  ramcl2  16948  0ram  16952  strfv  17136  imasaddfnlem  17473  imasaddvallem  17474  acsfn1  17604  drsdirfi  18257  sylow2a  19486  gsumpt  19829  dprdfadd  19889  ablfac1eulem  19941  pgpfaclem1  19950  acsfn1p  20414  rsp1  20848  mplcoe1  21591  mplcoe5  21594  mdetunilem9  22121  opnnei  22623  iscnp4  22766  cnpnei  22767  hausnei2  22856  fiuncmp  22907  llycmpkgen2  23053  1stckgen  23057  ptbasfi  23084  xkoccn  23122  xkoptsub  23157  ptcmpfi  23316  cnextcn  23570  tsmsid  23643  ustuqtop3  23747  utopreg  23756  prdsdsf  23872  prdsmet  23875  prdsbl  23999  fsumcn  24385  itgfsum  25343  dvmptfsum  25491  elply2  25709  elplyd  25715  ply1term  25717  ply0  25721  plymullem  25729  jensenlem1  26488  jensenlem2  26489  frcond3  29519  h1de2bi  30802  spansni  30805  gsumle  32237  gsumvsca1  32366  gsumvsca2  32367  1fldgenq  32407  mxidlirredi  32582  extdg1id  32737  ordtconnlem1  32899  cntnevol  33221  eulerpartgbij  33366  breprexpnat  33641  cvmlift2lem1  34288  cvmlift2lem12  34300  dfon2lem7  34756  bj-tagss  35856  lindsenlbs  36478  matunitlindflem1  36479  divrngidl  36891  isfldidl  36931  ispridlc  36933  pclfinclN  38816  osumcllem10N  38831  pexmidlem7N  38842  clsk1indlem4  42785  clsk1indlem1  42786  fourierdlem62  44874  pzriprnglem4  46798