Theorem elsni 4027

Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
elsni	|- ( A e. { B } -> A = B )

Proof of Theorem elsni

Step	Hyp	Ref	Expression
1		elsncg 4025	. 2 |- ( A e. { B } -> ( A e. { B } <-> A = B ) )
2	1	ibi 244	1 |- ( A e. { B } -> A = B )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1870   {csn 4002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-sn 4003

This theorem is referenced by:  elsnc2g  4032  elpwunsn  4043  eqoreldif  4044  disjsn2  4064  rabsnifsb  4071  sssn  4161  disjxsn  4420  opth1  4695  sosn  4924  ressn  5392  elsuci  5508  funcnvsn  5646  fvconst  6097  fnsnb  6098  fmptap  6102  fvunsn  6111  mpt2snif  6404  1stconst  6895  2ndconst  6896  reldmtpos  6989  tpostpos  7001  disjen  7735  map2xp  7748  ac6sfi  7821  ixpfi2  7878  elfi2  7934  fisn  7947  unxpwdom2  8103  cantnfp1lem3  8184  isfin4-3  8743  dcomex  8875  iundom2g  8963  fpwwe2lem13  9066  canthp1lem2  9077  0tsk  9179  elreal2  9555  ax1rid  9584  ltxrlt  9703  un0addcl  10903  un0mulcl  10904  elfzonlteqm1  11986  seqf1o  12251  seqid3  12254  seqz  12258  1exp  12298  hashnn0pnf  12522  hashprg  12569  cats1un  12817  fsumss  13769  sumsn  13785  fsum2dlem  13809  fsumcom2  13813  ackbijnn  13864  fprodss  13980  fprod2dlem  14012  fprodcom2  14016  fprodsplitsn  14021  lcmfunsnlem2lem1  14582  lcmfunsnlem2lem2  14583  phi1  14690  dfphi2  14691  nnnn0modprm0  14720  ramubcl  14939  0ram  14941  ramz  14946  imasvscafn  15394  xpsc0  15417  xpsc1  15418  xpsfrnel2  15422  mreexmrid  15500  2initoinv  15856  2termoinv  15863  gsumress  16470  gsumval2  16474  0nsg  16813  symgextf1lem  17012  symgextf1  17013  pmtrprfval  17079  psgnsn  17112  lsmdisj2  17267  subgdisj1  17276  lt6abl  17464  gsumsnfd  17519  gsumzunsnd  17523  gsumunsnfd  17524  gsum2dlem2  17538  dprdfeq0  17590  dprdsn  17604  dprd2da  17610  pgpfac1lem3a  17644  pgpfaclem2  17650  lsssn0  18106  lspsneq0  18170  lspdisjb  18284  lbsextlem4  18319  0ring01eq  18430  mplcoe5  18627  coe1tm  18801  frgpcyg  19075  obselocv  19222  obs2ss  19223  obslbs  19224  mat0dim0  19423  mat0dimid  19424  mat0dimscm  19425  mat1dimscm  19431  mavmul0g  19509  mdet0pr  19548  mdetunilem9  19576  cramer0  19646  pmatcollpw3fi1lem1  19741  basdif0  19899  ordtbas  20139  ordtrest2  20151  cmpfi  20354  refun0  20461  txdis1cn  20581  ptrescn  20585  txkgen  20598  xkoptsub  20600  ordthmeolem  20747  pt1hmeo  20752  filcon  20829  filufint  20866  flimclslem  20930  ptcmplem3  21000  idnghm  21675  iccpnfcnv  21868  iccpnfhmeo  21869  bndth  21882  ivthicc  22290  ovoliunlem1  22333  i1fima2sn  22515  i1f1  22525  itg1addlem4  22534  itg1addlem5  22535  i1fmulc  22538  limcres  22718  limccnp  22723  limccnp2  22724  degltlem1  22898  ply1rem  22989  fta1blem  22994  ig1pdvds  23002  plyeq0lem  23032  plypf1  23034  plyaddlem1  23035  plymullem1  23036  coemulhi  23076  plycj  23099  taylfval  23179  abelthlem3  23253  rlimcnp  23756  wilthlem2  23859  logexprlim  24016  tgldim0eq  24410  nbcusgra  25036  uvtxnbgra  25066  clwlkisclwwlklem2a4  25357  vdgr1d  25476  vdgr1b  25477  vdgr1a  25479  eupap1  25549  frgraunss  25568  vdgfrgragt2  25600  frgrancvvdeqlemC  25612  frgrawopreglem2  25618  gidsn  25921  rngosn  25977  rngoueqz  26003  xrge0tsmsbi  28388  submateqlem1  28472  submateqlem2  28473  ordtrest2NEW  28568  xrge0iifcnv  28578  xrge0iifhom  28582  qqhval2  28625  esumsnf  28724  esumpr  28726  esumiun  28754  measvunilem0  28874  measvuni  28875  carsggect  28979  omsmeas  28984  plymulx0  29224  bnj142OLD  29322  bnj98  29466  bnj1442  29646  bnj1452  29649  derangsn  29681  subfacp1lem5  29695  erdszelem4  29705  erdszelem8  29709  sconpi1  29750  cvmlift2lem6  29819  cvmlift2lem12  29825  onint1  30894  bj-1nel0  31296  bj-sngltag  31326  bj-projval  31339  tan2h  31641  ptrest  31643  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem28  31672  poimirlem29  31673  poimirlem30  31674  poimirlem31  31675  poimirlem32  31676  prdsbnd  31829  rrnequiv  31871  grpokerinj  31887  0rngo  31964  isdmn3  32011  dibelval2nd  34429  hdmaprnlem9N  35137  hdmap14lem4a  35151  hbtlem5  35693  flcidc  35739  frege133d  35996  radcnvrat  36300  unisnALT  36963  sumsnd  36987  fnchoice  36990  rnsnf  37081  founiiun0  37088  sumsnf  37223  fsumsplitsn  37224  cncfiooicc  37344  fperdvper  37362  dvnmul  37387  dvmptfprodlem  37388  dvnprodlem1  37390  dvnprodlem2  37391  itgcoscmulx  37415  stoweidlem44  37474  wallispi  37501  fourierdlem49  37587  fourierdlem56  37594  fourierdlem80  37618  fourierdlem93  37631  fourierdlem101  37639  sge00  37752  sge0sn  37755  sge0snmpt  37759  sge0iunmptlemfi  37789  sge0p1  37790  sge0fodjrnlem  37792  nnfoctbdjlem  37802  meadjiunlem  37812  ismeannd  37814  caratheodorylem1  37856  eldmressn  38024  iccpartltu  38138  nnsum3primesprm  38284  bgoldbtbndlem3  38301  c0snmgmhm  38681  zrinitorngc  38769  ldepspr  39035  lmod1zr  39055