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 2105  Vcvv 3473   ⊆ wss 3948  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  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  7158  limensuci  9159  domunfican  9326  finsschain  9365  epfrs  9732  tc2  9743  tcsni  9744  dju1dif  10173  fpwwe2lem12  10643  wunfi  10722  uniwun  10741  un0mulcl  12513  nn0ssz  12588  xrinfmss  13296  hashbclem  14418  hashf1lem1  14422  hashf1lem1OLD  14423  hashf1lem2  14424  fsum2dlem  15723  fsumabs  15754  fsumrlim  15764  fsumo1  15765  fsumiun  15774  incexclem  15789  fprod2dlem  15931  lcmfunsnlem  16585  lcmfun  16589  coprmprod  16605  coprmproddvdslem  16606  ramcl2  16956  0ram  16960  strfv  17144  imasaddfnlem  17481  imasaddvallem  17482  acsfn1  17612  drsdirfi  18268  sylow2a  19535  gsumpt  19878  dprdfadd  19938  ablfac1eulem  19990  pgpfaclem1  19999  acsfn1p  20646  rsp1  21087  pzriprnglem4  21344  mplcoe1  21903  mplcoe5  21906  mdetunilem9  22442  opnnei  22944  iscnp4  23087  cnpnei  23088  hausnei2  23177  fiuncmp  23228  llycmpkgen2  23374  1stckgen  23378  ptbasfi  23405  xkoccn  23443  xkoptsub  23478  ptcmpfi  23637  cnextcn  23891  tsmsid  23964  ustuqtop3  24068  utopreg  24077  prdsdsf  24193  prdsmet  24196  prdsbl  24320  fsumcn  24708  itgfsum  25676  dvmptfsum  25827  elply2  26048  elplyd  26054  ply1term  26056  ply0  26060  plymullem  26068  jensenlem1  26832  jensenlem2  26833  frcond3  29955  h1de2bi  31240  spansni  31243  gsumle  32678  gsumvsca1  32807  gsumvsca2  32808  1fldgenq  32848  mxidlirredi  33027  extdg1id  33196  ordtconnlem1  33368  cntnevol  33690  eulerpartgbij  33835  breprexpnat  34110  cvmlift2lem1  34757  cvmlift2lem12  34769  dfon2lem7  35231  bj-tagss  36325  lindsenlbs  36947  matunitlindflem1  36948  divrngidl  37360  isfldidl  37400  ispridlc  37402  pclfinclN  39285  osumcllem10N  39300  pexmidlem7N  39311  clsk1indlem4  43258  clsk1indlem1  43259  fourierdlem62  45343