Theorem snss 4749

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-sn 4590

This theorem is referenced by:  tpss  4801  sspwb  5409  nnullss  5422  exss  5423  pwssun  5530  fvimacnvi  7024  fvimacnv  7025  fvimacnvALT  7029  fnressn  7130  limensuci  9117  domunfican  9272  finsschain  9310  epfrs  9684  tc2  9695  tcsni  9696  dju1dif  10126  fpwwe2lem12  10595  wunfi  10674  uniwun  10693  un0mulcl  12476  nn0ssz  12552  xrinfmss  13270  hashbclem  14417  hashf1lem1  14420  hashf1lem2  14421  fsum2dlem  15736  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  incexclem  15802  fprod2dlem  15946  lcmfunsnlem  16611  lcmfun  16615  coprmprod  16631  coprmproddvdslem  16632  ramcl2  16987  0ram  16991  strfv  17173  imasaddfnlem  17491  imasaddvallem  17492  acsfn1  17622  drsdirfi  18266  sylow2a  19549  gsumpt  19892  dprdfadd  19952  ablfac1eulem  20004  pgpfaclem1  20013  acsfn1p  20708  rsp1  21147  pzriprnglem4  21394  mplcoe1  21944  mplcoe5  21947  mdetunilem9  22507  opnnei  23007  iscnp4  23150  cnpnei  23151  hausnei2  23240  fiuncmp  23291  llycmpkgen2  23437  1stckgen  23441  ptbasfi  23468  xkoccn  23506  xkoptsub  23541  ptcmpfi  23700  cnextcn  23954  tsmsid  24027  ustuqtop3  24131  utopreg  24140  prdsdsf  24255  prdsmet  24258  prdsbl  24379  fsumcn  24761  itgfsum  25728  dvmptfsum  25879  elply2  26101  elplyd  26107  ply1term  26109  ply0  26113  plymullem  26121  jensenlem1  26897  jensenlem2  26898  frcond3  30198  h1de2bi  31483  spansni  31486  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  1fldgenq  33272  unitprodclb  33360  mxidlirredi  33442  extdg1id  33661  ordtconnlem1  33914  cntnevol  34218  eulerpartgbij  34363  breprexpnat  34625  cvmlift2lem1  35289  cvmlift2lem12  35301  dfon2lem7  35777  bj-tagss  36968  lindsenlbs  37609  matunitlindflem1  37610  divrngidl  38022  isfldidl  38062  ispridlc  38064  pclfinclN  39944  osumcllem10N  39959  pexmidlem7N  39970  clsk1indlem4  44033  clsk1indlem1  44034  fourierdlem62  46166