Theorem elsni 4601

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

Assertion

Ref	Expression
elsni	⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Proof of Theorem elsni

Step	Hyp	Ref	Expression
1		elsng 4598	. 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
2	1	ibi 270	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4585

This theorem is used by:  elsnd  4602  elsn2g  4625  nelsn  4627  elpwunsn  4645  eqoreldif  4646  disjsn2  4673  rabsnifsb  4683  sssn  4787  disjxsn  5097  opth1  5451  sosn  5742  ressn  6283  elsnxp  6289  elsuci  6427  funcnvsn  6584  funopdmsn  7148  fvconst  7161  fnsnr  7162  fmptap  7169  mposnif  7530  resf1extb  7932  1stconst  8098  2ndconst  8099  reldmtpos  8233  tpostpos  8245  disjen  9133  map2xp  9146  en1eqsn  9246  ac6sfi  9255  ixpfi2  9318  elfi2  9385  fisn  9398  unxpwdom2  9561  cantnfp1lem3  9660  djulf1o  9918  djurf1o  9919  djur  9925  eldju2ndl  9930  eldju2ndr  9931  isfin4p1  10318  dcomex  10450  iundom2g  10549  fpwwe2lem12  10652  canthp1lem2  10663  0tsk  10765  elreal2  11142  ax1rid  11171  ltxrlt  11305  un0addcl  12562  un0mulcl  12563  fzodisjsn  13754  elfzonlteqm1  13798  elfzo0l  13813  elfzr  13838  elfzlmr  13839  seqf1o  14108  seqid3  14111  seqz  14115  1exp  14156  hashnn0pnf  14407  hash1elsn  14436  hashprg  14460  cats1un  14791  fsumss  15812  sumsnf  15830  fsumsplitsn  15831  fsum2dlem  15857  fsumcom2  15861  ackbijnn  15918  fprodss  16036  fprod2dlem  16068  fprodcom2  16072  fprodsplitsn  16077  sumeven  16478  sumodd  16479  divalgmod  16497  lcmfunsnlem2lem1  16729  lcmfunsnlem2lem2  16730  phi1  16865  dfphi2  16866  nnnn0modprm0  16899  ramubcl  17111  0ram  17113  ramz  17118  imasvscafn  17624  mreexmrid  17732  2initoinv  18100  2termoinv  18107  gsumress  18785  gsumval2  18789  smndex1basss  19018  smndex1mndlem  19022  0nsg  19293  symgextf1lem  19548  symgextf1  19549  pmtrprfval  19615  psgnsn  19648  lsmdisj2  19810  subgdisj1  19819  lt6abl  20023  gsumsnfd  20079  gsumzunsnd  20084  gsumunsnfd  20085  gsum2dlem2  20099  dprdfeq0  20152  dprdsn  20166  dprd2da  20172  pgpfac1lem3a  20206  pgpfaclem2  20212  ablsimpnosubgd  20234  c0snmgmhm  20604  0ring01eq  20691  zrinitorngc  20805  lsssn0  21133  lspsneq0  21197  lspdisjb  21314  pidlnz  21438  0ringprmidl  21541  pzriprnglem12  21706  frgpcyg  21787  obselocv  21942  obs2ss  21943  lindsenlbs  22065  mplcoe5  22257  psdmul  22395  coe1tm  22500  mat0dim0  22690  mat0dimid  22691  mat0dimscm  22692  mat1dimscm  22698  mavmul0g  22776  mdet0pr  22815  mdetunilem9  22843  matunitlindf  22904  cramer0  22916  pmatcollpw3fi1lem1  23012  basdif0  23179  ordtbas  23418  ordtrest2  23430  cmpfi  23634  refun0  23742  txdis1cn  23862  ptrescn  23866  txkgen  23879  xkoptsub  23881  ordthmeolem  24028  pt1hmeo  24033  filconn  24110  filufint  24147  flimclslem  24211  ptcmplem3  24281  idnghm  24970  iccpnfcnv  25173  iccpnfhmeo  25174  bndth  25187  ivthicc  25687  ovoliunlem1  25731  i1fima2sn  25909  i1f1  25919  itg1addlem4  25928  itg1addlem5  25929  i1fmulc  25932  limcres  26114  limccnp  26119  limccnp2  26120  degltlem1  26298  ply1rem  26392  fta1blem  26397  ig1pdvds  26406  plyeq0lem  26437  plypf1  26439  plyaddlem1  26440  plymullem1  26441  coemulhi  26481  plycj  26504  plycjOLD  26506  plyn0mulidp  26512  taylfval  26596  abelthlem3  26670  rlimcnp  27203  wilthlem2  27306  logexprlim  27462  2sqreultblem  27685  tgldim0eq  28846  edglnl  29601  nbgr1vtx  29819  vtxdginducedm1lem4  30003  clwlkclwwlklem2a4  30468  eucrct2eupth  30726  frgrncvvdeqlem9  30788  nsnlplig  30963  nsnlpligALT  30964  fsumiunle  33300  cshw1s2  33401  gsumhashmul  33508  xrge0tsmsbi  33515  gsumwrd2dccatlem  33518  cyc3evpm  33591  0ringcring  33693  elrspunidl  33857  drngmxidlr  33881  ig1pmindeg  34013  0mplrim  34025  selvply1rhmlemb  34030  mplmulmvr  34050  vieta  34091  lbslsat  34127  lindsunlem  34135  irngnminplynz  34223  ordtrest2NEW  34434  xrge0iifcnv  34444  xrge0iifhom  34448  esumsnf  34575  esumpr  34577  esumiun  34605  inelpisys  34666  measvunilem0  34725  measvuni  34726  carsggect  34830  omsmeas  34835  repr0  35120  bnj98  35377  bnj1442  35559  bnj1452  35562  subfacp1lem5  35764  erdszelem4  35774  erdszelem8  35778  sconnpi1  35819  cvmlift2lem6  35888  cvmlift2lem12  35894  fmla0xp  35963  onint1  37069  dfttc4lem2  37149  bj-1nel0  37699  bj-sngltag  37728  bj-projval  37741  bj-elsn0  37908  bj-fununsn1  38006  tan2h  38367  ptrest  38369  poimirlem23  38393  poimirlem24  38394  poimirlem25  38395  poimirlem28  38398  poimirlem29  38399  poimirlem30  38400  poimirlem31  38401  poimirlem32  38402  prdsbnd  38544  rrnequiv  38586  grpokerinj  38644  rngoueqz  38691  gidsn  38703  0rngo  38778  isdmn3  38825  dibelval2nd  42026  hdmaprnlem9N  42731  hdmap14lem4a  42745  dvrelog2b  42933  sticksstones11  43023  unitscyglem2  43063  0prjspnrel  43474  hbtlem5  43970  flcidc  44012  safesnsupfiss  44256  frege133d  44606  radcnvrat  45139  unisnALT  45749  sumsnd  45861  fnchoice  45864  rnsnf  46017  founiiun0  46023  elmapsnd  46036  fsneqrn  46042  infxrpnf  46275  supminfxr2  46298  cncfiooicc  46723  fperdvper  46748  dvmptfprodlem  46773  dvnprodlem1  46775  dvnprodlem2  46776  itgcoscmulx  46798  stoweidlem44  46873  fourierdlem49  46984  fourierdlem56  46991  fourierdlem80  47015  fourierdlem93  47028  fourierdlem101  47036  sge00  47205  sge0sn  47208  sge0snmpt  47212  sge0iunmptlemfi  47242  sge0p1  47243  sge0fodjrnlem  47245  sge0snmptf  47266  sge0splitsn  47270  nnfoctbdjlem  47284  meadjiunlem  47294  ismeannd  47296  caratheodorylem1  47355  isomenndlem  47359  hoidmv1le  47423  hoidmvlelem2  47425  hoidmvlelem3  47426  ovnhoilem1  47430  hoiqssbl  47454  ovnovollem1  47485  ovnovollem2  47486  eldmressn  47926  iccpartltu  48326  sbgoldbo  48704  nnsum3primesprm  48707  bgoldbtbndlem3  48724  stgr1  48878  gpgprismgr4cycllem7  49018  isidom3  49261  ldepspr  49404  lmod1zr  49424  termcbas2  50409  idfudiag1  50452