Theorem snss 4725

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

Syntax hints:   ↔ wb 205   ∈ wcel 2110  Vcvv 3431   ⊆ wss 3892  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-sn 4568

This theorem is referenced by:  tpss  4774  snelpw  5364  sspwb  5368  nnullss  5380  exss  5381  pwssun  5485  fvimacnvi  6924  fvimacnv  6925  fvimacnvALT  6929  fnressn  7025  limensuci  8920  domunfican  9063  finsschain  9102  epfrs  9487  tc2  9498  tcsni  9499  dju1dif  9927  fpwwe2lem12  10397  wunfi  10476  uniwun  10495  un0mulcl  12265  nn0ssz  12339  xrinfmss  13041  hashbclem  14160  hashf1lem1  14164  hashf1lem1OLD  14165  hashf1lem2  14166  fsum2dlem  15478  fsumabs  15509  fsumrlim  15519  fsumo1  15520  fsumiun  15529  incexclem  15544  fprod2dlem  15686  lcmfunsnlem  16342  lcmfun  16346  coprmprod  16362  coprmproddvdslem  16363  ramcl2  16713  0ram  16717  strfv  16901  imasaddfnlem  17235  imasaddvallem  17236  acsfn1  17366  drsdirfi  18019  sylow2a  19220  gsumpt  19559  dprdfadd  19619  ablfac1eulem  19671  pgpfaclem1  19680  acsfn1p  20063  rsp1  20491  mplcoe1  21234  mplcoe5  21237  mdetunilem9  21765  opnnei  22267  iscnp4  22410  cnpnei  22411  hausnei2  22500  fiuncmp  22551  llycmpkgen2  22697  1stckgen  22701  ptbasfi  22728  xkoccn  22766  xkoptsub  22801  ptcmpfi  22960  cnextcn  23214  tsmsid  23287  ustuqtop3  23391  utopreg  23400  prdsdsf  23516  prdsmet  23519  prdsbl  23643  fsumcn  24029  itgfsum  24987  dvmptfsum  25135  elply2  25353  elplyd  25359  ply1term  25361  ply0  25365  plymullem  25373  jensenlem1  26132  jensenlem2  26133  frcond3  28627  h1de2bi  29910  spansni  29913  gsumle  31344  gsumvsca1  31473  gsumvsca2  31474  extdg1id  31732  ordtconnlem1  31868  cntnevol  32190  eulerpartgbij  32333  breprexpnat  32608  cvmlift2lem1  33258  cvmlift2lem12  33270  dfon2lem7  33759  bj-tagss  35164  lindsenlbs  35766  matunitlindflem1  35767  divrngidl  36180  isfldidl  36220  ispridlc  36222  pclfinclN  37958  osumcllem10N  37973  pexmidlem7N  37984  clsk1indlem4  41622  clsk1indlem1  41623  fourierdlem62  43678