Theorem snss 4729

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  {csn 4568

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-sn 4569

This theorem is referenced by:  tpss  4781  sspwb  5396  nnullss  5409  exss  5410  pwssun  5516  fvimacnvi  6998  fvimacnv  6999  fvimacnvALT  7003  fnressn  7105  limensuci  9084  domunfican  9225  finsschain  9262  epfrs  9643  tc2  9652  tcsni  9653  dju1dif  10086  fpwwe2lem12  10556  wunfi  10635  uniwun  10654  un0mulcl  12462  nn0ssz  12538  xrinfmss  13253  hashbclem  14405  hashf1lem1  14408  hashf1lem2  14409  fsum2dlem  15723  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  incexclem  15792  fprod2dlem  15936  lcmfunsnlem  16601  lcmfun  16605  coprmprod  16621  coprmproddvdslem  16622  ramcl2  16978  0ram  16982  strfv  17164  imasaddfnlem  17483  imasaddvallem  17484  acsfn1  17618  drsdirfi  18262  sylow2a  19585  gsumpt  19928  dprdfadd  19988  ablfac1eulem  20040  pgpfaclem1  20049  gsumle  20111  acsfn1p  20767  rsp1  21227  pzriprnglem4  21474  mplcoe1  22025  mplcoe5  22028  mdetunilem9  22595  opnnei  23095  iscnp4  23238  cnpnei  23239  hausnei2  23328  fiuncmp  23379  llycmpkgen2  23525  1stckgen  23529  ptbasfi  23556  xkoccn  23594  xkoptsub  23629  ptcmpfi  23788  cnextcn  24042  tsmsid  24115  ustuqtop3  24218  utopreg  24227  prdsdsf  24342  prdsmet  24345  prdsbl  24466  fsumcn  24847  itgfsum  25804  dvmptfsum  25952  elply2  26171  elplyd  26177  ply1term  26179  ply0  26183  plymullem  26191  jensenlem1  26964  jensenlem2  26965  frcond3  30354  h1de2bi  31640  spansni  31643  gsumvsca1  33302  gsumvsca2  33303  1fldgenq  33398  unitprodclb  33464  mxidlirredi  33546  extdg1id  33826  ordtconnlem1  34084  cntnevol  34388  eulerpartgbij  34532  breprexpnat  34794  cvmlift2lem1  35500  cvmlift2lem12  35512  dfon2lem7  35985  axtco  36669  bj-tagss  37303  lindsenlbs  37950  matunitlindflem1  37951  divrngidl  38363  isfldidl  38403  ispridlc  38405  pclfinclN  40410  osumcllem10N  40425  pexmidlem7N  40436  clsk1indlem4  44489  clsk1indlem1  44490  fourierdlem62  46614  nthrucw  47332