Theorem elsni 4645

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sn 4629

This theorem is referenced by:  elsn2g  4666  nelsn  4668  elpwunsn  4687  eqoreldif  4688  disjsn2  4716  rabsnifsb  4726  sssn  4829  disjxsn  5141  opth1  5475  sosn  5762  ressn  6284  elsnxp  6290  elsuci  6431  funcnvsn  6598  funopdmsn  7150  fvconst  7164  fnsnr  7165  fmptap  7170  mposnif  7526  1stconst  8088  2ndconst  8089  reldmtpos  8221  tpostpos  8233  disjen  9136  map2xp  9149  en1eqsn  9276  ac6sfi  9289  ixpfi2  9352  elfi2  9411  fisn  9424  unxpwdom2  9585  cantnfp1lem3  9677  djulf1o  9909  djurf1o  9910  djur  9916  eldju2ndl  9921  eldju2ndr  9922  isfin4p1  10312  dcomex  10444  iundom2g  10537  fpwwe2lem12  10639  canthp1lem2  10650  0tsk  10752  elreal2  11129  ax1rid  11158  ltxrlt  11288  un0addcl  12509  un0mulcl  12510  fzodisjsn  13674  elfzonlteqm1  13712  elfzo0l  13726  elfzr  13749  elfzlmr  13750  seqf1o  14013  seqid3  14016  seqz  14020  1exp  14061  hashnn0pnf  14306  hash1elsn  14335  hashprg  14359  cats1un  14675  fsumss  15675  sumsnf  15693  fsumsplitsn  15694  fsum2dlem  15720  fsumcom2  15724  ackbijnn  15778  fprodss  15896  fprod2dlem  15928  fprodcom2  15932  fprodsplitsn  15937  sumeven  16334  sumodd  16335  divalgmod  16353  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  phi1  16710  dfphi2  16711  nnnn0modprm0  16743  ramubcl  16955  0ram  16957  ramz  16962  imasvscafn  17487  mreexmrid  17591  2initoinv  17964  2termoinv  17971  gsumress  18607  gsumval2  18611  smndex1basss  18822  smndex1mndlem  18826  0nsg  19085  symgextf1lem  19329  symgextf1  19330  pmtrprfval  19396  psgnsn  19429  lsmdisj2  19591  subgdisj1  19600  lt6abl  19804  gsumsnfd  19860  gsumzunsnd  19865  gsumunsnfd  19866  gsum2dlem2  19880  dprdfeq0  19933  dprdsn  19947  dprd2da  19953  pgpfac1lem3a  19987  pgpfaclem2  19993  ablsimpnosubgd  20015  c0snmgmhm  20353  0ring01eq  20418  lsssn0  20702  lspsneq0  20767  lspdisjb  20884  pzriprnglem12  21261  frgpcyg  21348  obselocv  21502  obs2ss  21503  mplcoe5  21814  coe1tm  22015  mat0dim0  22189  mat0dimid  22190  mat0dimscm  22191  mat1dimscm  22197  mavmul0g  22275  mdet0pr  22314  mdetunilem9  22342  cramer0  22412  pmatcollpw3fi1lem1  22508  basdif0  22676  ordtbas  22916  ordtrest2  22928  cmpfi  23132  refun0  23239  txdis1cn  23359  ptrescn  23363  txkgen  23376  xkoptsub  23378  ordthmeolem  23525  pt1hmeo  23530  filconn  23607  filufint  23644  flimclslem  23708  ptcmplem3  23778  idnghm  24480  iccpnfcnv  24684  iccpnfhmeo  24685  bndth  24698  ivthicc  25199  ovoliunlem1  25243  i1fima2sn  25421  i1f1  25431  itg1addlem4  25440  itg1addlem4OLD  25441  itg1addlem5  25442  i1fmulc  25445  limcres  25627  limccnp  25632  limccnp2  25633  degltlem1  25814  ply1rem  25905  fta1blem  25910  ig1pdvds  25918  plyeq0lem  25948  plypf1  25950  plyaddlem1  25951  plymullem1  25952  coemulhi  25992  plycj  26015  taylfval  26095  abelthlem3  26169  rlimcnp  26694  wilthlem2  26797  logexprlim  26952  2sqreultblem  27175  tgldim0eq  28009  edglnl  28658  nbgr1vtx  28870  vtxdginducedm1lem4  29054  clwlkclwwlklem2a4  29505  eucrct2eupth  29753  frgrncvvdeqlem9  29815  nsnlplig  29989  nsnlpligALT  29990  fsumiunle  32290  cshw1s2  32379  gsumhashmul  32466  xrge0tsmsbi  32468  cyc3evpm  32567  pidlnz  32750  elrspunidl  32808  0ringprmidl  32830  ig1pmindeg  32935  lbslsat  32977  lindsunlem  32985  irngnminplynz  33048  ordtrest2NEW  33189  xrge0iifcnv  33199  xrge0iifhom  33203  esumsnf  33348  esumpr  33350  esumiun  33378  inelpisys  33438  measvunilem0  33497  measvuni  33498  carsggect  33603  omsmeas  33608  plymulx0  33844  repr0  33909  bnj98  34164  bnj1442  34346  bnj1452  34349  subfacp1lem5  34461  erdszelem4  34471  erdszelem8  34475  sconnpi1  34516  cvmlift2lem6  34585  cvmlift2lem12  34591  fmla0xp  34660  onint1  35637  bj-1nel0  36138  bj-sngltag  36167  bj-projval  36180  bj-elsn0  36339  bj-fununsn1  36437  tan2h  36783  lindsenlbs  36786  matunitlindf  36789  ptrest  36790  poimirlem23  36814  poimirlem24  36815  poimirlem25  36816  poimirlem28  36819  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  poimirlem32  36823  prdsbnd  36964  rrnequiv  37006  grpokerinj  37064  rngoueqz  37111  gidsn  37123  0rngo  37198  isdmn3  37245  dibelval2nd  40326  hdmaprnlem9N  41031  hdmap14lem4a  41045  dvrelog2b  41237  sticksstones11  41278  0prjspnrel  41671  hbtlem5  42172  flcidc  42218  safesnsupfiss  42468  frege133d  42818  radcnvrat  43375  unisnALT  43989  sumsnd  44012  fnchoice  44015  rnsnf  44182  founiiun0  44188  elmapsnd  44202  fsneqrn  44209  infxrpnf  44455  supminfxr2  44478  cncfiooicc  44909  fperdvper  44934  dvmptfprodlem  44959  dvnprodlem1  44961  dvnprodlem2  44962  itgcoscmulx  44984  stoweidlem44  45059  fourierdlem49  45170  fourierdlem56  45177  fourierdlem80  45201  fourierdlem93  45214  fourierdlem101  45222  sge00  45391  sge0sn  45394  sge0snmpt  45398  sge0iunmptlemfi  45428  sge0p1  45429  sge0fodjrnlem  45431  sge0snmptf  45452  sge0splitsn  45456  nnfoctbdjlem  45470  meadjiunlem  45480  ismeannd  45482  caratheodorylem1  45541  isomenndlem  45545  hoidmv1le  45609  hoidmvlelem2  45611  hoidmvlelem3  45612  ovnhoilem1  45616  hoiqssbl  45640  ovnovollem1  45671  ovnovollem2  45672  eldmressn  46046  iccpartltu  46392  sbgoldbo  46754  nnsum3primesprm  46757  bgoldbtbndlem3  46774  zrinitorngc  46987  ldepspr  47242  lmod1zr  47262