Theorem snss 4736

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898  {csn 4575

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-sn 4576

This theorem is referenced by:  tpss  4788  sspwb  5392  nnullss  5405  exss  5406  pwssun  5511  fvimacnvi  6991  fvimacnv  6992  fvimacnvALT  6996  fnressn  7097  limensuci  9073  domunfican  9213  finsschain  9250  epfrs  9628  tc2  9637  tcsni  9638  dju1dif  10071  fpwwe2lem12  10540  wunfi  10619  uniwun  10638  un0mulcl  12422  nn0ssz  12498  xrinfmss  13211  hashbclem  14361  hashf1lem1  14364  hashf1lem2  14365  fsum2dlem  15679  fsumabs  15710  fsumrlim  15720  fsumo1  15721  fsumiun  15730  incexclem  15745  fprod2dlem  15889  lcmfunsnlem  16554  lcmfun  16558  coprmprod  16574  coprmproddvdslem  16575  ramcl2  16930  0ram  16934  strfv  17116  imasaddfnlem  17434  imasaddvallem  17435  acsfn1  17569  drsdirfi  18213  sylow2a  19533  gsumpt  19876  dprdfadd  19936  ablfac1eulem  19988  pgpfaclem1  19997  gsumle  20059  acsfn1p  20716  rsp1  21176  pzriprnglem4  21423  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  30251  h1de2bi  31536  spansni  31539  gsumvsca1  33202  gsumvsca2  33203  1fldgenq  33295  unitprodclb  33361  mxidlirredi  33443  extdg1id  33700  ordtconnlem1  33958  cntnevol  34262  eulerpartgbij  34406  breprexpnat  34668  cvmlift2lem1  35367  cvmlift2lem12  35379  dfon2lem7  35852  bj-tagss  37045  lindsenlbs  37676  matunitlindflem1  37677  divrngidl  38089  isfldidl  38129  ispridlc  38131  pclfinclN  40070  osumcllem10N  40085  pexmidlem7N  40096  clsk1indlem4  44162  clsk1indlem1  44163  fourierdlem62  46291  nthrucw  47009