Theorem snss 4348

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

Syntax hints:   ↔ wb 196   ∈ wcel 2030  Vcvv 3231   ⊆ wss 3607  {csn 4210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-sn 4211

This theorem is referenced by:  snssgOLD  4349  prssOLD  4384  tpss  4400  snelpw  4943  sspwb  4947  nnullss  4960  exss  4961  pwssun  5049  relsnOLD  5260  fvimacnvi  6371  fvimacnv  6372  fvimacnvALT  6376  fnressn  6465  limensuci  8177  domunfican  8274  finsschain  8314  epfrs  8645  tc2  8656  tcsni  8657  cda1dif  9036  fpwwe2lem13  9502  wunfi  9581  uniwun  9600  un0mulcl  11365  nn0ssz  11436  xrinfmss  12178  hashbclem  13274  hashf1lem1  13277  hashf1lem2  13278  fsum2dlem  14545  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  incexclem  14612  fprod2dlem  14754  lcmfunsnlem  15401  lcmfun  15405  coprmprod  15422  coprmproddvdslem  15423  ramcl2  15767  0ram  15771  strfv  15954  imasaddfnlem  16235  imasaddvallem  16236  acsfn1  16369  drsdirfi  16985  sylow2a  18080  gsumpt  18407  dprdfadd  18465  ablfac1eulem  18517  pgpfaclem1  18526  rsp1  19272  mplcoe1  19513  mplcoe5  19516  mdetunilem9  20474  opnnei  20972  iscnp4  21115  cnpnei  21116  hausnei2  21205  fiuncmp  21255  llycmpkgen2  21401  1stckgen  21405  ptbasfi  21432  xkoccn  21470  xkoptsub  21505  ptcmpfi  21664  cnextcn  21918  tsmsid  21990  ustuqtop3  22094  utopreg  22103  prdsdsf  22219  prdsmet  22222  prdsbl  22343  fsumcn  22720  itgfsum  23638  dvmptfsum  23783  elply2  23997  elplyd  24003  ply1term  24005  ply0  24009  plymullem  24017  jensenlem1  24758  jensenlem2  24759  frcond3  27249  h1de2bi  28541  spansni  28544  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  ordtconnlem1  30098  cntnevol  30419  eulerpartgbij  30562  breprexpnat  30840  cvmlift2lem1  31410  cvmlift2lem12  31422  dfon2lem7  31818  bj-tagss  33093  lindsenlbs  33534  matunitlindflem1  33535  divrngidl  33957  isfldidl  33997  ispridlc  33999  pclfinclN  35554  osumcllem10N  35569  pexmidlem7N  35580  acsfn1p  38086  clsk1indlem4  38659  clsk1indlem1  38660  fourierdlem62  40703