Theorem snss 4723

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  Vcvv 3432   ⊆ wss 3890  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-sn 4563

This theorem is referenced by:  tpss  4775  sspwb  5395  nnullss  5408  exss  5409  pwssun  5517  fvimacnvi  7000  fvimacnv  7001  fvimacnvALT  7005  fnressn  7108  limensuci  9088  domunfican  9229  finsschain  9266  epfrs  9650  tc2  9659  tcsni  9660  dju1dif  10093  fpwwe2lem12  10563  wunfi  10642  uniwun  10661  un0mulcl  12469  nn0ssz  12545  xrinfmss  13260  hashbclem  14412  hashf1lem1  14415  hashf1lem2  14416  fsum2dlem  15730  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  incexclem  15799  fprod2dlem  15943  lcmfunsnlem  16608  lcmfun  16612  coprmprod  16628  coprmproddvdslem  16629  ramcl2  16985  0ram  16989  strfv  17171  imasaddfnlem  17490  imasaddvallem  17491  acsfn1  17625  drsdirfi  18269  sylow2a  19592  gsumpt  19935  dprdfadd  19995  ablfac1eulem  20047  pgpfaclem1  20056  gsumle  20118  acsfn1p  20778  rsp1  21237  pzriprnglem4  21466  mplcoe1  22020  mplcoe5  22023  mdetunilem9  22610  opnnei  23110  iscnp4  23253  cnpnei  23254  hausnei2  23343  fiuncmp  23394  llycmpkgen2  23540  1stckgen  23544  ptbasfi  23571  xkoccn  23609  xkoptsub  23644  ptcmpfi  23803  cnextcn  24057  tsmsid  24130  ustuqtop3  24233  utopreg  24242  prdsdsf  24357  prdsmet  24360  prdsbl  24481  fsumcn  24862  itgfsum  25819  dvmptfsum  25967  elply2  26186  elplyd  26192  ply1term  26194  ply0  26198  plymullem  26206  jensenlem1  26975  jensenlem2  26976  frcond3  30364  h1de2bi  31650  spansni  31653  gsumvsca1  33314  gsumvsca2  33315  1fldgenq  33413  unitprodclb  33479  mxidlirredi  33561  extdg1id  33857  ordtconnlem1  34115  cntnevol  34419  eulerpartgbij  34563  breprexpnat  34825  cvmlift2lem1  35537  cvmlift2lem12  35549  dfon2lem7  36022  axtco  36706  bj-tagss  37340  lindsenlbs  37989  matunitlindflem1  37990  divrngidl  38402  isfldidl  38442  ispridlc  38444  pclfinclN  40449  osumcllem10N  40464  pexmidlem7N  40475  clsk1indlem4  44495  clsk1indlem1  44496  fourierdlem62  46618  nthrucw  47338