Theorem snss 4719

Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4718). 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 4718	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Syntax hints:   ↔ wb 205   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887  {csn 4561

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-sn 4562

This theorem is referenced by:  tpss  4768  snelpw  5361  sspwb  5365  nnullss  5377  exss  5378  pwssun  5485  fvimacnvi  6929  fvimacnv  6930  fvimacnvALT  6934  fnressn  7030  limensuci  8940  domunfican  9087  finsschain  9126  epfrs  9489  tc2  9500  tcsni  9501  dju1dif  9928  fpwwe2lem12  10398  wunfi  10477  uniwun  10496  un0mulcl  12267  nn0ssz  12341  xrinfmss  13044  hashbclem  14164  hashf1lem1  14168  hashf1lem1OLD  14169  hashf1lem2  14170  fsum2dlem  15482  fsumabs  15513  fsumrlim  15523  fsumo1  15524  fsumiun  15533  incexclem  15548  fprod2dlem  15690  lcmfunsnlem  16346  lcmfun  16350  coprmprod  16366  coprmproddvdslem  16367  ramcl2  16717  0ram  16721  strfv  16905  imasaddfnlem  17239  imasaddvallem  17240  acsfn1  17370  drsdirfi  18023  sylow2a  19224  gsumpt  19563  dprdfadd  19623  ablfac1eulem  19675  pgpfaclem1  19684  acsfn1p  20067  rsp1  20495  mplcoe1  21238  mplcoe5  21241  mdetunilem9  21769  opnnei  22271  iscnp4  22414  cnpnei  22415  hausnei2  22504  fiuncmp  22555  llycmpkgen2  22701  1stckgen  22705  ptbasfi  22732  xkoccn  22770  xkoptsub  22805  ptcmpfi  22964  cnextcn  23218  tsmsid  23291  ustuqtop3  23395  utopreg  23404  prdsdsf  23520  prdsmet  23523  prdsbl  23647  fsumcn  24033  itgfsum  24991  dvmptfsum  25139  elply2  25357  elplyd  25363  ply1term  25365  ply0  25369  plymullem  25377  jensenlem1  26136  jensenlem2  26137  frcond3  28633  h1de2bi  29916  spansni  29919  gsumle  31350  gsumvsca1  31479  gsumvsca2  31480  extdg1id  31738  ordtconnlem1  31874  cntnevol  32196  eulerpartgbij  32339  breprexpnat  32614  cvmlift2lem1  33264  cvmlift2lem12  33276  dfon2lem7  33765  bj-tagss  35170  lindsenlbs  35772  matunitlindflem1  35773  divrngidl  36186  isfldidl  36226  ispridlc  36228  pclfinclN  37964  osumcllem10N  37979  pexmidlem7N  37990  clsk1indlem4  41654  clsk1indlem1  41655  fourierdlem62  43709