Theorem snss 4766

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3464   ⊆ wss 3931  {csn 4606

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-sn 4607

This theorem is referenced by:  tpss  4818  sspwb  5429  nnullss  5442  exss  5443  pwssun  5550  fvimacnvi  7047  fvimacnv  7048  fvimacnvALT  7052  fnressn  7153  limensuci  9172  domunfican  9338  finsschain  9376  epfrs  9750  tc2  9761  tcsni  9762  dju1dif  10192  fpwwe2lem12  10661  wunfi  10740  uniwun  10759  un0mulcl  12540  nn0ssz  12616  xrinfmss  13331  hashbclem  14475  hashf1lem1  14478  hashf1lem2  14479  fsum2dlem  15791  fsumabs  15822  fsumrlim  15832  fsumo1  15833  fsumiun  15842  incexclem  15857  fprod2dlem  16001  lcmfunsnlem  16665  lcmfun  16669  coprmprod  16685  coprmproddvdslem  16686  ramcl2  17041  0ram  17045  strfv  17227  imasaddfnlem  17547  imasaddvallem  17548  acsfn1  17678  drsdirfi  18322  sylow2a  19605  gsumpt  19948  dprdfadd  20008  ablfac1eulem  20060  pgpfaclem1  20069  acsfn1p  20764  rsp1  21203  pzriprnglem4  21450  mplcoe1  22000  mplcoe5  22003  mdetunilem9  22563  opnnei  23063  iscnp4  23206  cnpnei  23207  hausnei2  23296  fiuncmp  23347  llycmpkgen2  23493  1stckgen  23497  ptbasfi  23524  xkoccn  23562  xkoptsub  23597  ptcmpfi  23756  cnextcn  24010  tsmsid  24083  ustuqtop3  24187  utopreg  24196  prdsdsf  24311  prdsmet  24314  prdsbl  24435  fsumcn  24817  itgfsum  25785  dvmptfsum  25936  elply2  26158  elplyd  26164  ply1term  26166  ply0  26170  plymullem  26178  jensenlem1  26954  jensenlem2  26955  frcond3  30255  h1de2bi  31540  spansni  31543  gsumle  33097  gsumvsca1  33228  gsumvsca2  33229  1fldgenq  33321  unitprodclb  33409  mxidlirredi  33491  extdg1id  33712  ordtconnlem1  33960  cntnevol  34264  eulerpartgbij  34409  breprexpnat  34671  cvmlift2lem1  35329  cvmlift2lem12  35341  dfon2lem7  35812  bj-tagss  37003  lindsenlbs  37644  matunitlindflem1  37645  divrngidl  38057  isfldidl  38097  ispridlc  38099  pclfinclN  39974  osumcllem10N  39989  pexmidlem7N  40000  clsk1indlem4  44043  clsk1indlem1  44044  fourierdlem62  46177