Theorem elsn 1820

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15.

Assertion

Ref	Expression
elsn	⊢ (x ∈ {A} ↔ x = A)

Distinct variable group(s):   x,A

Proof of Theorem elsn

Step	Hyp	Ref	Expression
1		df-sn 1811	. 2 ⊢ {A} = {x∣x = A}
2	1	cleqabi 1176	1 ⊢ (x ∈ {A} ↔ x = A)

Syntax hints:   ↔ wb 127   = wceq 1091   ∈ wcel 1092  {csn 1808

This theorem is referenced by:  dfpr2 1821  disjsn 1836  snprc 1838  snss 1849  snsspw 1857  rext 1862  exss 1881  pwpw0 1883  eusn 1913  uni0b 1939  iunxsn 2034  frirr 2176  onmindif2 2313  suceloni 2314  fconstopab 2448  imasn 2616  elimasn 2617  fconst 2774  fv2 2828  fvopabn 2873  fsn 2895  fconstfv 2903  fvclss 2907  ec2 3203  snec 3232  map1 3335  xpsnen 3339  pw2en 3348  eirrv 3449  sucprcreg 3451  ranksn 3532  aceq5lem1 3558  aceq5lem2 3559  aceq5lem4 3561  kmlem3 3582  kmlem4 3583  kmlem10 3589  cfsuc 3709  elreal 4044  infxpidmlem8 4940  hsn0elch 5155  h1deot 5454

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-sn 1811

metamath.org