Theorem snss 4728

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889  {csn 4567

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-sn 4568

This theorem is referenced by:  tpss  4780  sspwb  5401  nnullss  5414  exss  5415  pwssun  5523  fvimacnvi  7004  fvimacnv  7005  fvimacnvALT  7009  fnressn  7112  limensuci  9091  domunfican  9232  finsschain  9269  epfrs  9652  tc2  9661  tcsni  9662  dju1dif  10095  fpwwe2lem12  10565  wunfi  10644  uniwun  10663  un0mulcl  12471  nn0ssz  12547  xrinfmss  13262  hashbclem  14414  hashf1lem1  14417  hashf1lem2  14418  fsum2dlem  15732  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  incexclem  15801  fprod2dlem  15945  lcmfunsnlem  16610  lcmfun  16614  coprmprod  16630  coprmproddvdslem  16631  ramcl2  16987  0ram  16991  strfv  17173  imasaddfnlem  17492  imasaddvallem  17493  acsfn1  17627  drsdirfi  18271  sylow2a  19594  gsumpt  19937  dprdfadd  19997  ablfac1eulem  20049  pgpfaclem1  20058  gsumle  20120  acsfn1p  20776  rsp1  21235  pzriprnglem4  21464  mplcoe1  22015  mplcoe5  22018  mdetunilem9  22585  opnnei  23085  iscnp4  23228  cnpnei  23229  hausnei2  23318  fiuncmp  23369  llycmpkgen2  23515  1stckgen  23519  ptbasfi  23546  xkoccn  23584  xkoptsub  23619  ptcmpfi  23778  cnextcn  24032  tsmsid  24105  ustuqtop3  24208  utopreg  24217  prdsdsf  24332  prdsmet  24335  prdsbl  24456  fsumcn  24837  itgfsum  25794  dvmptfsum  25942  elply2  26161  elplyd  26167  ply1term  26169  ply0  26173  plymullem  26181  jensenlem1  26950  jensenlem2  26951  frcond3  30339  h1de2bi  31625  spansni  31628  gsumvsca1  33287  gsumvsca2  33288  1fldgenq  33383  unitprodclb  33449  mxidlirredi  33531  extdg1id  33810  ordtconnlem1  34068  cntnevol  34372  eulerpartgbij  34516  breprexpnat  34778  cvmlift2lem1  35484  cvmlift2lem12  35496  dfon2lem7  35969  axtco  36653  bj-tagss  37287  lindsenlbs  37936  matunitlindflem1  37937  divrngidl  38349  isfldidl  38389  ispridlc  38391  pclfinclN  40396  osumcllem10N  40411  pexmidlem7N  40422  clsk1indlem4  44471  clsk1indlem1  44472  fourierdlem62  46596  nthrucw  47316