Theorem elsni 4646

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 4643	. 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-sn 4630

This theorem is referenced by:  elsn2g  4667  nelsn  4669  elpwunsn  4688  eqoreldif  4689  disjsn2  4717  rabsnifsb  4727  sssn  4830  disjxsn  5141  opth1  5477  sosn  5764  ressn  6289  elsnxp  6295  elsuci  6436  funcnvsn  6603  funopdmsn  7159  fvconst  7173  fnsnr  7174  fmptap  7179  mposnif  7536  1stconst  8105  2ndconst  8106  reldmtpos  8240  tpostpos  8252  disjen  9159  map2xp  9172  en1eqsn  9299  ac6sfi  9312  ixpfi2  9375  elfi2  9438  fisn  9451  unxpwdom2  9612  cantnfp1lem3  9704  djulf1o  9936  djurf1o  9937  djur  9943  eldju2ndl  9948  eldju2ndr  9949  isfin4p1  10339  dcomex  10471  iundom2g  10564  fpwwe2lem12  10666  canthp1lem2  10677  0tsk  10779  elreal2  11156  ax1rid  11185  ltxrlt  11315  un0addcl  12536  un0mulcl  12537  fzodisjsn  13703  elfzonlteqm1  13741  elfzo0l  13755  elfzr  13778  elfzlmr  13779  seqf1o  14041  seqid3  14044  seqz  14048  1exp  14089  hashnn0pnf  14334  hash1elsn  14363  hashprg  14387  cats1un  14704  fsumss  15704  sumsnf  15722  fsumsplitsn  15723  fsum2dlem  15749  fsumcom2  15753  ackbijnn  15807  fprodss  15925  fprod2dlem  15957  fprodcom2  15961  fprodsplitsn  15966  sumeven  16364  sumodd  16365  divalgmod  16383  lcmfunsnlem2lem1  16609  lcmfunsnlem2lem2  16610  phi1  16742  dfphi2  16743  nnnn0modprm0  16775  ramubcl  16987  0ram  16989  ramz  16994  imasvscafn  17519  mreexmrid  17623  2initoinv  17999  2termoinv  18006  gsumress  18642  gsumval2  18646  smndex1basss  18857  smndex1mndlem  18861  0nsg  19124  symgextf1lem  19375  symgextf1  19376  pmtrprfval  19442  psgnsn  19475  lsmdisj2  19637  subgdisj1  19646  lt6abl  19850  gsumsnfd  19906  gsumzunsnd  19911  gsumunsnfd  19912  gsum2dlem2  19926  dprdfeq0  19979  dprdsn  19993  dprd2da  19999  pgpfac1lem3a  20033  pgpfaclem2  20039  ablsimpnosubgd  20061  c0snmgmhm  20401  0ring01eq  20466  zrinitorngc  20575  lsssn0  20832  lspsneq0  20896  lspdisjb  21014  pzriprnglem12  21418  frgpcyg  21507  obselocv  21662  obs2ss  21663  mplcoe5  21978  psdmul  22090  coe1tm  22192  mat0dim0  22382  mat0dimid  22383  mat0dimscm  22384  mat1dimscm  22390  mavmul0g  22468  mdet0pr  22507  mdetunilem9  22535  cramer0  22605  pmatcollpw3fi1lem1  22701  basdif0  22869  ordtbas  23109  ordtrest2  23121  cmpfi  23325  refun0  23432  txdis1cn  23552  ptrescn  23556  txkgen  23569  xkoptsub  23571  ordthmeolem  23718  pt1hmeo  23723  filconn  23800  filufint  23837  flimclslem  23901  ptcmplem3  23971  idnghm  24673  iccpnfcnv  24882  iccpnfhmeo  24883  bndth  24897  ivthicc  25400  ovoliunlem1  25444  i1fima2sn  25622  i1f1  25632  itg1addlem4  25641  itg1addlem4OLD  25642  itg1addlem5  25643  i1fmulc  25646  limcres  25828  limccnp  25833  limccnp2  25834  degltlem1  26021  ply1rem  26113  fta1blem  26118  ig1pdvds  26127  plyeq0lem  26157  plypf1  26159  plyaddlem1  26160  plymullem1  26161  coemulhi  26201  plycj  26225  taylfval  26306  abelthlem3  26383  rlimcnp  26910  wilthlem2  27014  logexprlim  27171  2sqreultblem  27394  tgldim0eq  28320  edglnl  28969  nbgr1vtx  29184  vtxdginducedm1lem4  29369  clwlkclwwlklem2a4  29820  eucrct2eupth  30068  frgrncvvdeqlem9  30130  nsnlplig  30304  nsnlpligALT  30305  fsumiunle  32605  cshw1s2  32694  gsumhashmul  32783  xrge0tsmsbi  32785  cyc3evpm  32884  pidlnz  33100  elrspunidl  33157  0ringprmidl  33178  ig1pmindeg  33272  lbslsat  33314  lindsunlem  33322  irngnminplynz  33382  ordtrest2NEW  33524  xrge0iifcnv  33534  xrge0iifhom  33538  esumsnf  33683  esumpr  33685  esumiun  33713  inelpisys  33773  measvunilem0  33832  measvuni  33833  carsggect  33938  omsmeas  33943  plymulx0  34179  repr0  34243  bnj98  34498  bnj1442  34680  bnj1452  34683  subfacp1lem5  34794  erdszelem4  34804  erdszelem8  34808  sconnpi1  34849  cvmlift2lem6  34918  cvmlift2lem12  34924  fmla0xp  34993  onint1  35933  bj-1nel0  36433  bj-sngltag  36462  bj-projval  36475  bj-elsn0  36634  bj-fununsn1  36732  tan2h  37085  lindsenlbs  37088  matunitlindf  37091  ptrest  37092  poimirlem23  37116  poimirlem24  37117  poimirlem25  37118  poimirlem28  37121  poimirlem29  37122  poimirlem30  37123  poimirlem31  37124  poimirlem32  37125  prdsbnd  37266  rrnequiv  37308  grpokerinj  37366  rngoueqz  37413  gidsn  37425  0rngo  37500  isdmn3  37547  dibelval2nd  40625  hdmaprnlem9N  41330  hdmap14lem4a  41344  dvrelog2b  41537  sticksstones11  41628  0prjspnrel  42051  hbtlem5  42552  flcidc  42598  safesnsupfiss  42845  frege133d  43195  radcnvrat  43751  unisnALT  44365  sumsnd  44388  fnchoice  44391  rnsnf  44557  founiiun0  44563  elmapsnd  44577  fsneqrn  44584  infxrpnf  44828  supminfxr2  44851  cncfiooicc  45282  fperdvper  45307  dvmptfprodlem  45332  dvnprodlem1  45334  dvnprodlem2  45335  itgcoscmulx  45357  stoweidlem44  45432  fourierdlem49  45543  fourierdlem56  45550  fourierdlem80  45574  fourierdlem93  45587  fourierdlem101  45595  sge00  45764  sge0sn  45767  sge0snmpt  45771  sge0iunmptlemfi  45801  sge0p1  45802  sge0fodjrnlem  45804  sge0snmptf  45825  sge0splitsn  45829  nnfoctbdjlem  45843  meadjiunlem  45853  ismeannd  45855  caratheodorylem1  45914  isomenndlem  45918  hoidmv1le  45982  hoidmvlelem2  45984  hoidmvlelem3  45985  ovnhoilem1  45989  hoiqssbl  46013  ovnovollem1  46044  ovnovollem2  46045  eldmressn  46419  iccpartltu  46765  sbgoldbo  47127  nnsum3primesprm  47130  bgoldbtbndlem3  47147  ldepspr  47541  lmod1zr  47561