Theorem snss 4679

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

Syntax hints:   ↔ wb 209   ∈ wcel 2111  Vcvv 3441   ⊆ wss 3881  {csn 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-sn 4526

This theorem is referenced by:  tpss  4728  snelpw  5303  sspwb  5307  nnullss  5319  exss  5320  pwssun  5421  fvimacnvi  6799  fvimacnv  6800  fvimacnvALT  6804  fnressn  6897  limensuci  8677  domunfican  8775  finsschain  8815  epfrs  9157  tc2  9168  tcsni  9169  dju1dif  9583  fpwwe2lem13  10053  wunfi  10132  uniwun  10151  un0mulcl  11919  nn0ssz  11991  xrinfmss  12691  hashbclem  13806  hashf1lem1  13809  hashf1lem2  13810  fsum2dlem  15117  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  incexclem  15183  fprod2dlem  15326  lcmfunsnlem  15975  lcmfun  15979  coprmprod  15995  coprmproddvdslem  15996  ramcl2  16342  0ram  16346  strfv  16523  imasaddfnlem  16793  imasaddvallem  16794  acsfn1  16924  drsdirfi  17540  sylow2a  18736  gsumpt  19075  dprdfadd  19135  ablfac1eulem  19187  pgpfaclem1  19196  acsfn1p  19571  rsp1  19990  mplcoe1  20705  mplcoe5  20708  mdetunilem9  21225  opnnei  21725  iscnp4  21868  cnpnei  21869  hausnei2  21958  fiuncmp  22009  llycmpkgen2  22155  1stckgen  22159  ptbasfi  22186  xkoccn  22224  xkoptsub  22259  ptcmpfi  22418  cnextcn  22672  tsmsid  22745  ustuqtop3  22849  utopreg  22858  prdsdsf  22974  prdsmet  22977  prdsbl  23098  fsumcn  23475  itgfsum  24430  dvmptfsum  24578  elply2  24793  elplyd  24799  ply1term  24801  ply0  24805  plymullem  24813  jensenlem1  25572  jensenlem2  25573  frcond3  28054  h1de2bi  29337  spansni  29340  gsumle  30775  gsumvsca1  30904  gsumvsca2  30905  extdg1id  31141  ordtconnlem1  31277  cntnevol  31597  eulerpartgbij  31740  breprexpnat  32015  cvmlift2lem1  32662  cvmlift2lem12  32674  dfon2lem7  33147  bj-tagss  34416  lindsenlbs  35052  matunitlindflem1  35053  divrngidl  35466  isfldidl  35506  ispridlc  35508  pclfinclN  37246  osumcllem10N  37261  pexmidlem7N  37272  clsk1indlem4  40747  clsk1indlem1  40748  fourierdlem62  42810