Theorem snss 4737

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3902  {csn 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-sn 4577

This theorem is referenced by:  tpss  4789  sspwb  5390  nnullss  5402  exss  5403  pwssun  5508  fvimacnvi  6985  fvimacnv  6986  fvimacnvALT  6990  fnressn  7091  limensuci  9066  domunfican  9206  finsschain  9243  epfrs  9621  tc2  9630  tcsni  9631  dju1dif  10064  fpwwe2lem12  10533  wunfi  10612  uniwun  10631  un0mulcl  12415  nn0ssz  12491  xrinfmss  13209  hashbclem  14359  hashf1lem1  14362  hashf1lem2  14363  fsum2dlem  15677  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  incexclem  15743  fprod2dlem  15887  lcmfunsnlem  16552  lcmfun  16556  coprmprod  16572  coprmproddvdslem  16573  ramcl2  16928  0ram  16932  strfv  17114  imasaddfnlem  17432  imasaddvallem  17433  acsfn1  17567  drsdirfi  18211  sylow2a  19532  gsumpt  19875  dprdfadd  19935  ablfac1eulem  19987  pgpfaclem1  19996  gsumle  20058  acsfn1p  20715  rsp1  21175  pzriprnglem4  21422  mplcoe1  21973  mplcoe5  21976  mdetunilem9  22536  opnnei  23036  iscnp4  23179  cnpnei  23180  hausnei2  23269  fiuncmp  23320  llycmpkgen2  23466  1stckgen  23470  ptbasfi  23497  xkoccn  23535  xkoptsub  23570  ptcmpfi  23729  cnextcn  23983  tsmsid  24056  ustuqtop3  24159  utopreg  24168  prdsdsf  24283  prdsmet  24286  prdsbl  24407  fsumcn  24789  itgfsum  25756  dvmptfsum  25907  elply2  26129  elplyd  26135  ply1term  26137  ply0  26141  plymullem  26149  jensenlem1  26925  jensenlem2  26926  frcond3  30247  h1de2bi  31532  spansni  31535  gsumvsca1  33193  gsumvsca2  33194  1fldgenq  33286  unitprodclb  33352  mxidlirredi  33434  extdg1id  33677  ordtconnlem1  33935  cntnevol  34239  eulerpartgbij  34383  breprexpnat  34645  cvmlift2lem1  35344  cvmlift2lem12  35356  dfon2lem7  35829  bj-tagss  37020  lindsenlbs  37661  matunitlindflem1  37662  divrngidl  38074  isfldidl  38114  ispridlc  38116  pclfinclN  39995  osumcllem10N  40010  pexmidlem7N  40021  clsk1indlem4  44083  clsk1indlem1  44084  fourierdlem62  46212