Theorem elsn 3748

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   <-> wb 176   = wceq 1642   e. wcel 1710  {csn 3737

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-sn 3741

This theorem is referenced by:  dfpr2  3749  ralsns  3763  rexsns  3764  disjsn  3786  snprc  3788  euabsn2  3791  snss  3838  difprsnss  3846  pwpw0  3855  eqsn  3867  snsspw  3877  pwsnALT  3882  dfnfc2  3909  uni0b  3916  uni0c  3917  axprimlem1  4088  pwadjoin  4119  pw10  4161  pw1sn  4165  eqpw1uni  4330  nnsucelrlem2  4425  opeliunxp  4820  dmsnopg  5066  nfunsn  5353  fsn  5432  fconstfv  5456  foundex  5914  el2c  6191  csucex  6259  nmembers1lem3  6270  nchoicelem6  6294