Theorem elsn 3251

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

Syntax hints:   <-> wb 219   = wceq 1586   e. wcel 1588  {csn 3238

This theorem is referenced by:  dfpr2 3252  rexsng 3265  ralsng 3276  disjsn 3280  snprc 3282  euabsn 3285  snss 3317  difprsn 3321  pwpw0 3326  eqsn 3332  snsspw 3337  pwsnALT 3362  hbeqel 3384  uni0b 3389  uni0c 3390  iinxsng 3495  iunxsn 3497  rext 3666  exss 3679  frirr 3789  trsuc2 3896  suceloni 4037  fconstopab 4166  dmsnop 4472  iunfopab 4639  fv2 4761  nfunsn 4792  dffv2 4820  fvopabn 4835  fsn 4899  fopabap 4909  fconstfv 4917  fvclss 4924  opabex3 4933  fparlem3 5206  fparlem4 5207  dfec2 5482  snec 5516  ixp0x 5579  xpsnen 5658  pw2en 5671  ac6sfilem3 5674  fimax 5846  indexfi 5878  elirrv 5933  sucprcreg 5935  ranksn 6036  aceq5lem1 6189  aceq5lem2 6190  aceq5lem4 6192  fodomnumlem 6208  onacda 6259  axdc4lem 6310  axcclem 6312  elreal 6768  xrsupexmnf 7623  xrinfmexpnf 7624  snunioolem 7929  fzsuc 8041  fzsn 8047  fzpr 8048  fseq1p1m1lem1 8062  infxpidmlem8OLD 9222  divalgmod 9303  1nprm 9366  sn0top 9768  cctop 9773  sncld 9930  grpsn 10209  ablsn 10302  gapmlem 10330  ringsn 10359  oefil2 11113  elfilmap 11150  zrdivrng 11256  hsn0elch 11587  h1deoi 11939  bnj112 13239  bnj141 13253  bnj145 13257  bnj158 13263  bnj521 13295  ghomsn 14368  dffr5 14463  wfrlem14 14623  wfrlem15 14624  elsingles 14775  dfiota3 14777  fates 14992  restidsing 15101  cbicplem 15247  iscst4 15261  prsubrtr 15497  sbtpsines 15667  idtrgrp 15756  invtrgrp 15757  ccid 16187  cptclsscpt 16256  alexsublem2 16262  alexsublem3 16263  alexsublem4 16264  locfincomp 16338  ist1-2 16366  ist1-3 16367  isufil2 16389  filssufillem 16394  filssufil 16395  ufileulem 16396  ufileu 16397  filcon 16404  flimcls 16412  cnpfillim 16413  opabex3OLD 16525  fimaxOLD 16570  indexfiOLD 16579  fzfi 16610  heiborlem18 16796  pi1fval 16916  0idl 16997  smprngpr 17024  isdmn3 17046  snssiALTVD 17484  snssiALT 17485  pointpsub 18183

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1593  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-sn 3242

Copyright terms: Public domain