Theorem snss 4755

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  Vcvv 3458   ⊆ wss 3908  {csn 4594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-sn 4595

This theorem is used by:  tpss  4807  sspwb  5435  nnullss  5448  exss  5449  pwssun  5558  fvimacnvi  7054  fvimacnv  7055  fvimacnvALT  7059  fnressn  7162  limensuci  9151  domunfican  9291  finsschain  9326  epfrs  9710  tc2  9719  tcsni  9720  dju1dif  10175  fpwwe2lem12  10645  wunfi  10724  uniwun  10743  un0mulcl  12556  nn0ssz  12632  xrinfmss  13354  hashbclem  14509  hashf1lem1  14512  hashf1lem2  14513  fsum2dlem  15847  fsumabs  15879  fsumrlim  15889  fsumo1  15890  fsumiun  15899  incexclem  15916  fprod2dlem  16060  lcmfunsnlem  16724  lcmfun  16728  coprmprod  16744  coprmproddvdslem  16745  ramcl2  17101  0ram  17105  strfv  17288  imasaddfnlem  17607  imasaddvallem  17608  acsfn1  17742  drsdirfi  18386  sylow2a  19720  gsumpt  20063  dprdfadd  20123  ablfac1eulem  20175  pgpfaclem1  20184  gsumle  20246  acsfn1p  20939  rsp1  21403  pzriprnglem4  21671  mplcoe1  22225  mplcoe5  22228  mdetunilem9  22814  opnnei  23314  iscnp4  23457  cnpnei  23458  hausnei2  23547  fiuncmp  23598  llycmpkgen2  23744  1stckgen  23748  ptbasfi  23775  xkoccn  23813  xkoptsub  23848  ptcmpfi  24007  cnextcn  24261  tsmsid  24334  ustuqtop3  24437  utopreg  24446  prdsdsf  24561  prdsmet  24564  prdsbl  24685  fsumcn  25066  itgfsum  26023  dvmptfsum  26171  elply2  26390  elplyd  26396  ply1term  26398  ply0  26402  plymullem  26410  jensenlem1  27188  jensenlem2  27189  frcond3  30657  h1de2bi  31943  spansni  31946  gsumvsca1  33577  gsumvsca2  33578  1fldgenq  33674  unitprodclb  33733  mxidlirredi  33785  extdg1id  34087  ordtconnlem1  34345  cntnevol  34650  eulerpartgbij  34794  breprexpnat  35053  cvmlift2lem1  35815  cvmlift2lem12  35827  dfon2lem7  36300  axtco  37023  bj-tagss  37657  lindsenlbs  38307  matunitlindflem1  38308  divrngidl  38720  isfldidl  38760  ispridlc  38762  pclfinclN  40765  osumcllem10N  40780  pexmidlem7N  40791  clsk1indlem4  44811  clsk1indlem1  44812  fourierdlem62  46923  nthrucw  47648