Theorem snss 4716

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-sn 4559

This theorem is referenced by:  tpss  4765  snelpw  5355  sspwb  5359  nnullss  5371  exss  5372  pwssun  5476  fvimacnvi  6911  fvimacnv  6912  fvimacnvALT  6916  fnressn  7012  limensuci  8889  domunfican  9017  finsschain  9056  epfrs  9420  tc2  9431  tcsni  9432  dju1dif  9859  fpwwe2lem12  10329  wunfi  10408  uniwun  10427  un0mulcl  12197  nn0ssz  12271  xrinfmss  12973  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  fsum2dlem  15410  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  incexclem  15476  fprod2dlem  15618  lcmfunsnlem  16274  lcmfun  16278  coprmprod  16294  coprmproddvdslem  16295  ramcl2  16645  0ram  16649  strfv  16833  imasaddfnlem  17156  imasaddvallem  17157  acsfn1  17287  drsdirfi  17938  sylow2a  19139  gsumpt  19478  dprdfadd  19538  ablfac1eulem  19590  pgpfaclem1  19599  acsfn1p  19982  rsp1  20408  mplcoe1  21148  mplcoe5  21151  mdetunilem9  21677  opnnei  22179  iscnp4  22322  cnpnei  22323  hausnei2  22412  fiuncmp  22463  llycmpkgen2  22609  1stckgen  22613  ptbasfi  22640  xkoccn  22678  xkoptsub  22713  ptcmpfi  22872  cnextcn  23126  tsmsid  23199  ustuqtop3  23303  utopreg  23312  prdsdsf  23428  prdsmet  23431  prdsbl  23553  fsumcn  23939  itgfsum  24896  dvmptfsum  25044  elply2  25262  elplyd  25268  ply1term  25270  ply0  25274  plymullem  25282  jensenlem1  26041  jensenlem2  26042  frcond3  28534  h1de2bi  29817  spansni  29820  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  extdg1id  31640  ordtconnlem1  31776  cntnevol  32096  eulerpartgbij  32239  breprexpnat  32514  cvmlift2lem1  33164  cvmlift2lem12  33176  dfon2lem7  33671  bj-tagss  35097  lindsenlbs  35699  matunitlindflem1  35700  divrngidl  36113  isfldidl  36153  ispridlc  36155  pclfinclN  37891  osumcllem10N  37906  pexmidlem7N  37917  clsk1indlem4  41543  clsk1indlem1  41544  fourierdlem62  43599