Theorem elsn 2418

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 2409	. 2 |- {A} = {x | x = A}
2	1	abeq2i 1568	1 |- (x e. {A} <-> x = A)

Syntax hints:   <-> wb 146   = wceq 955   e. wcel 957  {csn 2406

This theorem is referenced by:  dfpr2 2419  disjsn 2438  snprc 2440  eusn 2443  snss 2458  difprsn 2462  pwpw0 2466  eqsn 2471  snsspw 2476  uni0b 2519  uni0c 2520  iunid 2599  iunxsn 2608  sbcsng 2749  rext 2750  exss 2765  frirr 2920  suceloni 3058  fconstopab 3206  imasng 3420  elimasn 3422  fconst 3653  fv2 3715  fvopabn 3781  fsn 3829  fopabsn 3835  fopabap 3836  fconstfv 3844  fvclss 3850  2ndconst 4090  dfec2 4257  snec 4289  ixp0x 4352  xpsnen 4424  pw2en 4435  elirrv 4581  sucprcreg 4583  ranksn 4672  aceq5lem1 4718  aceq5lem2 4719  aceq5lem4 4721  elreal 5233  xrsupexmnf 6031  xrinfmexpnf 6032  snunioolem 6360  infxpidmlem8 7519  sn0top 7607  cctop 7612  sncld 7747  grpsn 8088  ablsn 8089  ringsn 8127  hsn0elch 9075  h1deot 9427  ghomsn 10344  oefil2 10500

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-sn 2409

Copyright terms: Public domain