Theorem elsn 3789

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

Syntax hints:   <-> wb 177   = wceq 1649   e. wcel 1721   {csn 3774

This theorem is referenced by:  dfpr2  3790  ralsns  3804  rexsns  3805  disjsn  3828  snprc  3831  euabsn2  3835  snss  3886  difprsnss  3894  pwpw0  3906  eqsn  3920  snsspw  3930  pwsnALT  3970  dfnfc2  3993  uni0b  4000  uni0c  4001  sndisj  4164  rext  4372  moabex  4382  exss  4386  reusv6OLD  4693  suceloni  4752  fconstmpt  4880  opeliunxp  4888  dmsnopg  5300  dfmpt3  5526  nfunsn  5720  dffv2  5755  fsn  5865  fnasrn  5871  fconstfv  5913  fvclss  5939  opabex3d  5948  opabex3  5949  eusvobj2  6541  oarec  6764  ixp0x  7049  xpsnen  7151  marypha2lem2  7399  elirrv  7521  sucprcreg  7523  cantnfp1lem1  7590  cantnfp1lem3  7592  dfac5lem1  7960  dfac5lem2  7961  dfac5lem4  7963  fin1a2lem11  8246  axdc4lem  8291  axcclem  8293  xrsupexmnf  10839  xrinfmexpnf  10840  iccid  10917  fzsn  11050  fzpr  11057  seqz  11326  hashf1  11661  fsum2dlem  12509  incexc2  12573  ef0lem  12636  divalgmod  12881  1nprm  13039  isprm2lem  13041  vdwapun  13297  xpsc0  13740  xpsc1  13741  gsumvallem1  14726  gex1  15180  sylow2alem1  15206  lsmdisj2  15269  0frgp  15366  0cyg  15457  prmcyg  15458  dprddisj2  15552  ablfacrp  15579  lspdisj  16152  lidlnz  16254  psrlidm  16422  mplcoe1  16483  mplcoe2  16485  mulgrhm2  16743  ocvin  16856  en2top  17005  restsn  17188  ist1-3  17367  ordtt1  17397  cmpcld  17419  ptopn2  17569  snfil  17849  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  haustsms2  18119  tsmsxplem1  18135  tsmsxplem2  18136  ust0  18202  dscopn  18574  nmoid  18729  limcdif  19716  ellimc2  19717  limcmpt  19723  limcres  19726  evlslem1  19889  ply1remlem  20038  plyeq0lem  20082  plyremlem  20174  aaliou2  20210  radcnv0  20285  abelthlem2  20301  wilthlem2  20805  vmappw  20852  ppinprm  20888  chtnprm  20890  musumsum  20930  dchrhash  21008  lgsquadlem1  21091  lgsquadlem2  21092  isusgra0  21329  nbcusgra  21425  usgrasscusgra  21445  grposn  21756  ablosn  21888  hsn0elch  22703  kerf1hrm  24215  xrge0iifiso  24274  qqhval2  24319  esumnul  24396  esumfzf  24412  sibfof  24607  sconpi1  24879  ghomsn  25052  prodsn  25239  fprod2dlem  25257  dffr5  25324  wfrlem14  25483  wfrlem15  25484  brsingle  25670  dfiota3  25676  funpartfun  25696  dfrdg4  25703  0idl  26525  smprngopr  26552  isdmn3  26574  pellexlem5  26786  jm2.23  26957  flcidc  27247  funressnfv  27859  dfdfat2  27862  tz6.12-afv  27904  raldifsnb  27946  otiunsndisj  27954  otiunsndisjX  27955  frgrancvvdeqlem9  28144  frgrawopreglem4  28150  usg2spot2nb  28168  snssiALTVD  28648  snssiALT  28649  bnj145  28800  bnj521  28810  lshpdisj  29470  lsat0cv  29516  snatpsubN  30232  dibelval3  31630  dib1dim  31648  dvh2dim  31928  mapd0  32148  hdmap14lem13  32366

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-sn 3780