Theorem snss 4790

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949  {csn 4629

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-sn 4630

This theorem is referenced by:  tpss  4839  sspwb  5450  nnullss  5463  exss  5464  pwssun  5572  fvimacnvi  7054  fvimacnv  7055  fvimacnvALT  7059  fnressn  7156  limensuci  9153  domunfican  9320  finsschain  9359  epfrs  9726  tc2  9737  tcsni  9738  dju1dif  10167  fpwwe2lem12  10637  wunfi  10716  uniwun  10735  un0mulcl  12506  nn0ssz  12581  xrinfmss  13289  hashbclem  14411  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1lem2  14417  fsum2dlem  15716  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  incexclem  15782  fprod2dlem  15924  lcmfunsnlem  16578  lcmfun  16582  coprmprod  16598  coprmproddvdslem  16599  ramcl2  16949  0ram  16953  strfv  17137  imasaddfnlem  17474  imasaddvallem  17475  acsfn1  17605  drsdirfi  18258  sylow2a  19487  gsumpt  19830  dprdfadd  19890  ablfac1eulem  19942  pgpfaclem1  19951  acsfn1p  20415  rsp1  20849  mplcoe1  21592  mplcoe5  21595  mdetunilem9  22122  opnnei  22624  iscnp4  22767  cnpnei  22768  hausnei2  22857  fiuncmp  22908  llycmpkgen2  23054  1stckgen  23058  ptbasfi  23085  xkoccn  23123  xkoptsub  23158  ptcmpfi  23317  cnextcn  23571  tsmsid  23644  ustuqtop3  23748  utopreg  23757  prdsdsf  23873  prdsmet  23876  prdsbl  24000  fsumcn  24386  itgfsum  25344  dvmptfsum  25492  elply2  25710  elplyd  25716  ply1term  25718  ply0  25722  plymullem  25730  jensenlem1  26491  jensenlem2  26492  frcond3  29522  h1de2bi  30807  spansni  30810  gsumle  32242  gsumvsca1  32371  gsumvsca2  32372  1fldgenq  32412  mxidlirredi  32587  extdg1id  32742  ordtconnlem1  32904  cntnevol  33226  eulerpartgbij  33371  breprexpnat  33646  cvmlift2lem1  34293  cvmlift2lem12  34305  dfon2lem7  34761  bj-tagss  35861  lindsenlbs  36483  matunitlindflem1  36484  divrngidl  36896  isfldidl  36936  ispridlc  36938  pclfinclN  38821  osumcllem10N  38836  pexmidlem7N  38847  clsk1indlem4  42795  clsk1indlem1  42796  fourierdlem62  44884  pzriprnglem4  46808