Theorem elsni 4618

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sn 4602

This theorem is referenced by:  elsnd  4619  elsn2g  4640  nelsn  4642  elpwunsn  4660  eqoreldif  4661  disjsn2  4688  rabsnifsb  4698  sssn  4802  disjxsn  5113  opth1  5450  sosn  5741  ressn  6274  elsnxp  6280  elsuci  6420  funcnvsn  6585  funopdmsn  7139  fvconst  7153  fnsnr  7154  fmptap  7161  mposnif  7521  resf1extb  7928  1stconst  8097  2ndconst  8098  reldmtpos  8231  tpostpos  8243  disjen  9146  map2xp  9159  en1eqsn  9278  ac6sfi  9290  ixpfi2  9360  elfi2  9424  fisn  9437  unxpwdom2  9600  cantnfp1lem3  9692  djulf1o  9924  djurf1o  9925  djur  9931  eldju2ndl  9936  eldju2ndr  9937  isfin4p1  10327  dcomex  10459  iundom2g  10552  fpwwe2lem12  10654  canthp1lem2  10665  0tsk  10767  elreal2  11144  ax1rid  11173  ltxrlt  11303  un0addcl  12532  un0mulcl  12533  fzodisjsn  13712  elfzonlteqm1  13755  elfzo0l  13770  elfzr  13794  elfzlmr  13795  seqf1o  14059  seqid3  14062  seqz  14066  1exp  14107  hashnn0pnf  14358  hash1elsn  14387  hashprg  14411  cats1un  14737  fsumss  15739  sumsnf  15757  fsumsplitsn  15758  fsum2dlem  15784  fsumcom2  15788  ackbijnn  15842  fprodss  15962  fprod2dlem  15994  fprodcom2  15998  fprodsplitsn  16003  sumeven  16404  sumodd  16405  divalgmod  16423  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  phi1  16790  dfphi2  16791  nnnn0modprm0  16824  ramubcl  17036  0ram  17038  ramz  17043  imasvscafn  17549  mreexmrid  17653  2initoinv  18021  2termoinv  18028  gsumress  18658  gsumval2  18662  smndex1basss  18881  smndex1mndlem  18885  0nsg  19150  symgextf1lem  19399  symgextf1  19400  pmtrprfval  19466  psgnsn  19499  lsmdisj2  19661  subgdisj1  19670  lt6abl  19874  gsumsnfd  19930  gsumzunsnd  19935  gsumunsnfd  19936  gsum2dlem2  19950  dprdfeq0  20003  dprdsn  20017  dprd2da  20023  pgpfac1lem3a  20057  pgpfaclem2  20063  ablsimpnosubgd  20085  c0snmgmhm  20420  0ring01eq  20487  zrinitorngc  20600  lsssn0  20903  lspsneq0  20967  lspdisjb  21085  pzriprnglem12  21451  frgpcyg  21532  obselocv  21686  obs2ss  21687  mplcoe5  21996  psdmul  22102  coe1tm  22208  mat0dim0  22403  mat0dimid  22404  mat0dimscm  22405  mat1dimscm  22411  mavmul0g  22489  mdet0pr  22528  mdetunilem9  22556  cramer0  22626  pmatcollpw3fi1lem1  22722  basdif0  22889  ordtbas  23128  ordtrest2  23140  cmpfi  23344  refun0  23451  txdis1cn  23571  ptrescn  23575  txkgen  23588  xkoptsub  23590  ordthmeolem  23737  pt1hmeo  23742  filconn  23819  filufint  23856  flimclslem  23920  ptcmplem3  23990  idnghm  24680  iccpnfcnv  24891  iccpnfhmeo  24892  bndth  24906  ivthicc  25409  ovoliunlem1  25453  i1fima2sn  25631  i1f1  25641  itg1addlem4  25650  itg1addlem5  25651  i1fmulc  25654  limcres  25837  limccnp  25842  limccnp2  25843  degltlem1  26027  ply1rem  26121  fta1blem  26126  ig1pdvds  26135  plyeq0lem  26165  plypf1  26167  plyaddlem1  26168  plymullem1  26169  coemulhi  26209  plycj  26233  plycjOLD  26235  taylfval  26316  abelthlem3  26393  rlimcnp  26925  wilthlem2  27029  logexprlim  27186  2sqreultblem  27409  tgldim0eq  28428  edglnl  29068  nbgr1vtx  29283  vtxdginducedm1lem4  29468  clwlkclwwlklem2a4  29924  eucrct2eupth  30172  frgrncvvdeqlem9  30234  nsnlplig  30408  nsnlpligALT  30409  fsumiunle  32754  cshw1s2  32882  gsumhashmul  33001  xrge0tsmsbi  33003  gsumwrd2dccatlem  33006  cyc3evpm  33107  0ringcring  33193  pidlnz  33337  elrspunidl  33389  0ringprmidl  33410  drngmxidlr  33439  ig1pmindeg  33557  lbslsat  33602  lindsunlem  33610  irngnminplynz  33692  ordtrest2NEW  33900  xrge0iifcnv  33910  xrge0iifhom  33914  esumsnf  34041  esumpr  34043  esumiun  34071  inelpisys  34131  measvunilem0  34190  measvuni  34191  carsggect  34296  omsmeas  34301  plymulx0  34525  repr0  34589  bnj98  34844  bnj1442  35026  bnj1452  35029  subfacp1lem5  35152  erdszelem4  35162  erdszelem8  35166  sconnpi1  35207  cvmlift2lem6  35276  cvmlift2lem12  35282  fmla0xp  35351  onint1  36413  bj-1nel0  36918  bj-sngltag  36947  bj-projval  36960  bj-elsn0  37119  bj-fununsn1  37217  tan2h  37582  lindsenlbs  37585  matunitlindf  37588  ptrest  37589  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem28  37618  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  prdsbnd  37763  rrnequiv  37805  grpokerinj  37863  rngoueqz  37910  gidsn  37922  0rngo  37997  isdmn3  38044  dibelval2nd  41117  hdmaprnlem9N  41822  hdmap14lem4a  41836  dvrelog2b  42025  sticksstones11  42115  unitscyglem2  42155  0prjspnrel  42597  hbtlem5  43099  flcidc  43141  safesnsupfiss  43386  frege133d  43736  radcnvrat  44286  unisnALT  44898  sumsnd  44998  fnchoice  45001  rnsnf  45156  founiiun0  45162  elmapsnd  45176  fsneqrn  45183  infxrpnf  45421  supminfxr2  45444  cncfiooicc  45871  fperdvper  45896  dvmptfprodlem  45921  dvnprodlem1  45923  dvnprodlem2  45924  itgcoscmulx  45946  stoweidlem44  46021  fourierdlem49  46132  fourierdlem56  46139  fourierdlem80  46163  fourierdlem93  46176  fourierdlem101  46184  sge00  46353  sge0sn  46356  sge0snmpt  46360  sge0iunmptlemfi  46390  sge0p1  46391  sge0fodjrnlem  46393  sge0snmptf  46414  sge0splitsn  46418  nnfoctbdjlem  46432  meadjiunlem  46442  ismeannd  46444  caratheodorylem1  46503  isomenndlem  46507  hoidmv1le  46571  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem1  46578  hoiqssbl  46602  ovnovollem1  46633  ovnovollem2  46634  eldmressn  47014  iccpartltu  47387  sbgoldbo  47749  nnsum3primesprm  47752  bgoldbtbndlem3  47769  stgr1  47921  gpgprismgr4cycllem7  48048  ldepspr  48397  lmod1zr  48417  termcbas2  49315  idfudiag1  49358