Theorem elsni 4594

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {csn 4577

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4578

This theorem is referenced by:  elsnd  4595  elsn2g  4616  nelsn  4618  elpwunsn  4636  eqoreldif  4637  disjsn2  4664  rabsnifsb  4674  sssn  4777  disjxsn  5086  opth1  5418  sosn  5706  ressn  6233  elsnxp  6239  elsuci  6376  funcnvsn  6532  funopdmsn  7084  fvconst  7098  fnsnr  7099  fmptap  7106  mposnif  7465  resf1extb  7867  1stconst  8033  2ndconst  8034  reldmtpos  8167  tpostpos  8179  disjen  9051  map2xp  9064  en1eqsn  9164  ac6sfi  9173  ixpfi2  9240  elfi2  9304  fisn  9317  unxpwdom2  9480  cantnfp1lem3  9576  djulf1o  9808  djurf1o  9809  djur  9815  eldju2ndl  9820  eldju2ndr  9821  isfin4p1  10209  dcomex  10341  iundom2g  10434  fpwwe2lem12  10536  canthp1lem2  10547  0tsk  10649  elreal2  11026  ax1rid  11055  ltxrlt  11186  un0addcl  12417  un0mulcl  12418  fzodisjsn  13600  elfzonlteqm1  13644  elfzo0l  13659  elfzr  13683  elfzlmr  13684  seqf1o  13950  seqid3  13953  seqz  13957  1exp  13998  hashnn0pnf  14249  hash1elsn  14278  hashprg  14302  cats1un  14627  fsumss  15632  sumsnf  15650  fsumsplitsn  15651  fsum2dlem  15677  fsumcom2  15681  ackbijnn  15735  fprodss  15855  fprod2dlem  15887  fprodcom2  15891  fprodsplitsn  15896  sumeven  16298  sumodd  16299  divalgmod  16317  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  phi1  16684  dfphi2  16685  nnnn0modprm0  16718  ramubcl  16930  0ram  16932  ramz  16937  imasvscafn  17441  mreexmrid  17549  2initoinv  17917  2termoinv  17924  gsumress  18556  gsumval2  18560  smndex1basss  18779  smndex1mndlem  18783  0nsg  19048  symgextf1lem  19299  symgextf1  19300  pmtrprfval  19366  psgnsn  19399  lsmdisj2  19561  subgdisj1  19570  lt6abl  19774  gsumsnfd  19830  gsumzunsnd  19835  gsumunsnfd  19836  gsum2dlem2  19850  dprdfeq0  19903  dprdsn  19917  dprd2da  19923  pgpfac1lem3a  19957  pgpfaclem2  19963  ablsimpnosubgd  19985  c0snmgmhm  20347  0ring01eq  20414  zrinitorngc  20527  lsssn0  20851  lspsneq0  20915  lspdisjb  21033  pzriprnglem12  21399  frgpcyg  21480  obselocv  21635  obs2ss  21636  mplcoe5  21945  psdmul  22051  coe1tm  22157  mat0dim0  22352  mat0dimid  22353  mat0dimscm  22354  mat1dimscm  22360  mavmul0g  22438  mdet0pr  22477  mdetunilem9  22505  cramer0  22575  pmatcollpw3fi1lem1  22671  basdif0  22838  ordtbas  23077  ordtrest2  23089  cmpfi  23293  refun0  23400  txdis1cn  23520  ptrescn  23524  txkgen  23537  xkoptsub  23539  ordthmeolem  23686  pt1hmeo  23691  filconn  23768  filufint  23805  flimclslem  23869  ptcmplem3  23939  idnghm  24629  iccpnfcnv  24840  iccpnfhmeo  24841  bndth  24855  ivthicc  25357  ovoliunlem1  25401  i1fima2sn  25579  i1f1  25589  itg1addlem4  25598  itg1addlem5  25599  i1fmulc  25602  limcres  25785  limccnp  25790  limccnp2  25791  degltlem1  25975  ply1rem  26069  fta1blem  26074  ig1pdvds  26083  plyeq0lem  26113  plypf1  26115  plyaddlem1  26116  plymullem1  26117  coemulhi  26157  plycj  26181  plycjOLD  26183  taylfval  26264  abelthlem3  26341  rlimcnp  26873  wilthlem2  26977  logexprlim  27134  2sqreultblem  27357  tgldim0eq  28448  edglnl  29088  nbgr1vtx  29303  vtxdginducedm1lem4  29488  clwlkclwwlklem2a4  29941  eucrct2eupth  30189  frgrncvvdeqlem9  30251  nsnlplig  30425  nsnlpligALT  30426  fsumiunle  32775  cshw1s2  32903  gsumhashmul  33015  xrge0tsmsbi  33017  gsumwrd2dccatlem  33020  cyc3evpm  33093  0ringcring  33193  pidlnz  33314  elrspunidl  33366  0ringprmidl  33387  drngmxidlr  33416  ig1pmindeg  33535  lbslsat  33589  lindsunlem  33597  irngnminplynz  33685  ordtrest2NEW  33896  xrge0iifcnv  33906  xrge0iifhom  33910  esumsnf  34037  esumpr  34039  esumiun  34067  inelpisys  34127  measvunilem0  34186  measvuni  34187  carsggect  34292  omsmeas  34297  plymulx0  34521  repr0  34585  bnj98  34840  bnj1442  35022  bnj1452  35025  subfacp1lem5  35167  erdszelem4  35177  erdszelem8  35181  sconnpi1  35222  cvmlift2lem6  35291  cvmlift2lem12  35297  fmla0xp  35366  onint1  36433  bj-1nel0  36938  bj-sngltag  36967  bj-projval  36980  bj-elsn0  37139  bj-fununsn1  37237  tan2h  37602  lindsenlbs  37605  matunitlindf  37608  ptrest  37609  poimirlem23  37633  poimirlem24  37634  poimirlem25  37635  poimirlem28  37638  poimirlem29  37639  poimirlem30  37640  poimirlem31  37641  poimirlem32  37642  prdsbnd  37783  rrnequiv  37825  grpokerinj  37883  rngoueqz  37930  gidsn  37942  0rngo  38017  isdmn3  38064  dibelval2nd  41141  hdmaprnlem9N  41846  hdmap14lem4a  41860  dvrelog2b  42049  sticksstones11  42139  unitscyglem2  42179  0prjspnrel  42610  hbtlem5  43111  flcidc  43153  safesnsupfiss  43398  frege133d  43748  radcnvrat  44297  unisnALT  44909  sumsnd  45014  fnchoice  45017  rnsnf  45172  founiiun0  45178  elmapsnd  45192  fsneqrn  45199  infxrpnf  45435  supminfxr2  45458  cncfiooicc  45885  fperdvper  45910  dvmptfprodlem  45935  dvnprodlem1  45937  dvnprodlem2  45938  itgcoscmulx  45960  stoweidlem44  46035  fourierdlem49  46146  fourierdlem56  46153  fourierdlem80  46177  fourierdlem93  46190  fourierdlem101  46198  sge00  46367  sge0sn  46370  sge0snmpt  46374  sge0iunmptlemfi  46404  sge0p1  46405  sge0fodjrnlem  46407  sge0snmptf  46428  sge0splitsn  46432  nnfoctbdjlem  46446  meadjiunlem  46456  ismeannd  46458  caratheodorylem1  46517  isomenndlem  46521  hoidmv1le  46585  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnhoilem1  46592  hoiqssbl  46616  ovnovollem1  46647  ovnovollem2  46648  eldmressn  47031  iccpartltu  47419  sbgoldbo  47781  nnsum3primesprm  47784  bgoldbtbndlem3  47801  stgr1  47955  gpgprismgr4cycllem7  48095  ldepspr  48468  lmod1zr  48488  termcbas2  49477  idfudiag1  49520