Theorem elsn 2421

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

Assertion

Ref	Expression
elsn	|- (x e. {A} <-> x = A)

Distinct variable group:   x,A

Proof of Theorem elsn

Step	Hyp	Ref	Expression
1		df-sn 2412	. 2 |- {A} = {x | x = A}
2	1	abeq2i 1570	1 |- (x e. {A} <-> x = A)

Syntax hints:   <-> wb 146   = wceq 956   e. wcel 958  {csn 2409

This theorem is referenced by:  dfpr2 2422  disjsn 2441  snprc 2443  eusn 2446  snss 2461  difprsn 2465  pwpw0 2469  eqsn 2474  snsspw 2479  pwsnALT 2501  uni0b 2523  uni0c 2524  iunid 2603  iunxsn 2612  sbcsng 2753  rext 2754  exss 2769  frirr 2924  suceloni 3062  fconstopab 3210  imasng 3424  elimasn 3426  fconst 3658  fv2 3720  fvopabn 3786  fsn 3834  fopabsn 3840  fopabap 3841  fconstfv 3849  fvclss 3855  2ndconst 4097  dfec2 4264  snec 4296  ixp0x 4359  xpsnen 4435  pw2en 4446  elirrv 4598  sucprcreg 4600  ranksn 4689  aceq5lem1 4735  aceq5lem2 4736  aceq5lem4 4738  elreal 5250  xrsupexmnf 6074  xrinfmexpnf 6075  snunioolem 6414  infxpidmlem8 7559  sn0top 7647  cctop 7652  sncld 7787  grpsn 8124  ablsn 8125  ringsn 8163  hsn0elch 9120  h1deot 9472  ghomsn 10388  oefil2 10567

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-sn 2412

Copyright terms: Public domain