Theorem elsn 2479

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:   x,A

Proof of Theorem elsn

Step	Hyp	Ref	Expression
1		df-sn 2470	. 2 ⊢ {A} = {x∣x = A}
2	1	abeq2i 1613	1 ⊢ (x ∈ {A} ↔ x = A)

Syntax hints:   ↔ wb 144   = wceq 992   ∈ wcel 994  {csn 2467

This theorem is referenced by:  dfpr2 2480  ralsng 2489  sbcsng 2490  disjsn 2502  snprc 2504  eusn 2507  snss 2525  difprsn 2529  pwpw0 2533  eqsn 2539  snsspw 2544  pwsnALT 2566  uni0b 2590  uni0c 2591  iunxsn 2682  rext 2834  exss 2847  frirr 2954  suceloni 3170  fconstopab 3293  imasng 3516  elimasn 3518  fconst 3765  fv2 3831  fvopabn 3897  fsn 3948  fopabsn 3954  fopabap 3955  fconstfv 3963  fvclss 3969  fparlem3 4201  fparlem4 4202  dfec2 4404  snec 4437  ixp0x 4500  xpsnen 4576  pw2en 4587  ac6sfilem3 4590  elirrv 4741  sucprcreg 4743  ranksn 4835  aceq5lem1 4881  aceq5lem2 4882  aceq5lem4 4884  elreal 5404  xrsupexmnf 6242  xrinfmexpnf 6243  snunioolem 6541  fzsuc 6636  infxpidmlem8 7771  sn0top 7859  cctop 7862  sncld 7997  grpsn 8273  ablsn 8366  ringsn 8405  hsn0elch 9396  h1deoi 9748  ghomsn 10673  restidsing 10805  zrdivrng 10969  sbtpsines 11062  oefil2 11079  ccid 11412  cptclsscpt 11489  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  locfincomp 11575  ist1-2 11603  ist1-3 11604  isufil2 11650  filssufillem 11655  filssufil 11656  ufileulem 11657  ufileu 11658  filcon 11665  flimcls 11684  cnpfillim 11686  elfilmap 11690  gapmlem 11783  opabex3 11806  fimax 11837  indexf 11847  fzfi 11864  fzsn 11865  fzpr 11866  heiborlem18 12028

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-sn 2470

Copyright terms: Public domain