Theorem snss 4785

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-sn 4627

This theorem is referenced by:  tpss  4837  sspwb  5454  nnullss  5467  exss  5468  pwssun  5575  fvimacnvi  7072  fvimacnv  7073  fvimacnvALT  7077  fnressn  7178  limensuci  9193  domunfican  9361  finsschain  9399  epfrs  9771  tc2  9782  tcsni  9783  dju1dif  10213  fpwwe2lem12  10682  wunfi  10761  uniwun  10780  un0mulcl  12560  nn0ssz  12636  xrinfmss  13352  hashbclem  14491  hashf1lem1  14494  hashf1lem2  14495  fsum2dlem  15806  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  incexclem  15872  fprod2dlem  16016  lcmfunsnlem  16678  lcmfun  16682  coprmprod  16698  coprmproddvdslem  16699  ramcl2  17054  0ram  17058  strfv  17240  imasaddfnlem  17573  imasaddvallem  17574  acsfn1  17704  drsdirfi  18351  sylow2a  19637  gsumpt  19980  dprdfadd  20040  ablfac1eulem  20092  pgpfaclem1  20101  acsfn1p  20800  rsp1  21247  pzriprnglem4  21495  mplcoe1  22055  mplcoe5  22058  mdetunilem9  22626  opnnei  23128  iscnp4  23271  cnpnei  23272  hausnei2  23361  fiuncmp  23412  llycmpkgen2  23558  1stckgen  23562  ptbasfi  23589  xkoccn  23627  xkoptsub  23662  ptcmpfi  23821  cnextcn  24075  tsmsid  24148  ustuqtop3  24252  utopreg  24261  prdsdsf  24377  prdsmet  24380  prdsbl  24504  fsumcn  24894  itgfsum  25862  dvmptfsum  26013  elply2  26235  elplyd  26241  ply1term  26243  ply0  26247  plymullem  26255  jensenlem1  27030  jensenlem2  27031  frcond3  30288  h1de2bi  31573  spansni  31576  gsumle  33101  gsumvsca1  33232  gsumvsca2  33233  1fldgenq  33324  unitprodclb  33417  mxidlirredi  33499  extdg1id  33716  ordtconnlem1  33923  cntnevol  34229  eulerpartgbij  34374  breprexpnat  34649  cvmlift2lem1  35307  cvmlift2lem12  35319  dfon2lem7  35790  bj-tagss  36981  lindsenlbs  37622  matunitlindflem1  37623  divrngidl  38035  isfldidl  38075  ispridlc  38077  pclfinclN  39952  osumcllem10N  39967  pexmidlem7N  39978  clsk1indlem4  44057  clsk1indlem1  44058  fourierdlem62  46183