Theorem snss 4741

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-sn 4585

This theorem is used by:  tpss  4791  sspwb  5416  nnullss  5429  exss  5430  pwssun  5542  fvimacnvi  7052  fvimacnv  7053  fvimacnvALT  7057  fnressn  7163  limensuci  9176  domunfican  9317  finsschain  9352  epfrs  9736  tc2  9745  tcsni  9746  dju1dif  10255  fpwwe2lem12  10731  wunfi  10810  uniwun  10829  un0mulcl  12644  nn0ssz  12720  xrinfmss  13444  hashbclem  14601  hashf1lem1  14604  hashf1lem2  14605  fsum2dlem  15942  fsumabs  15974  fsumrlim  15984  fsumo1  15985  fsumiun  15994  incexclem  16011  fprod2dlem  16153  lcmfunsnlem  16822  lcmfun  16826  coprmprod  16842  coprmproddvdslem  16843  ramcl2  17200  0ram  17204  strfv  17387  imasaddfnlem  17706  imasaddvallem  17707  acsfn1  17841  drsdirfi  18485  sylow2a  19839  gsumpt  20182  dprdfadd  20242  ablfac1eulem  20294  pgpfaclem1  20303  gsumle  20365  acsfn1p  21062  rsp1  21526  pzriprnglem4  21796  lindsenlbs  22163  mplcoe1  22352  mplcoe5  22355  mdetunilem9  22941  matunitlindflem1  23000  opnnei  23444  iscnp4  23587  cnpnei  23588  hausnei2  23677  fiuncmp  23728  llycmpkgen2  23875  1stckgen  23879  ptbasfi  23906  xkoccn  23944  xkoptsub  23979  ptcmpfi  24138  cnextcn  24392  tsmsid  24465  ustuqtop3  24568  utopreg  24577  prdsdsf  24692  prdsmet  24695  prdsbl  24816  fsumcn  25197  itgfsum  26153  dvmptfsum  26301  elply2  26520  elplyd  26526  ply1term  26528  ply0  26532  plymullem  26541  jensenlem1  27320  jensenlem2  27321  frcond3  30876  h1de2bi  32162  spansni  32165  gsumvsca1  33834  gsumvsca2  33835  1fldgenq  33931  unitprodclb  33991  mxidlirredi  34043  extdg1id  34345  ordtconnlem1  34603  cntnevol  34908  eulerpartgbij  35051  breprexpnat  35310  cvmlift2lem1  36154  cvmlift2lem12  36166  dfon2lem7  36644  axtco  37352  bj-tagss  37986  divrngidl  39056  isfldidl  39096  ispridlc  39098  pclfinclN  41101  osumcllem10N  41116  pexmidlem7N  41127  clsk1indlem4  45138  clsk1indlem1  45139  fourierdlem62  47272  numtowerdt  48010