Theorem elsni 4599

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {csn 4582

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4583

This theorem is referenced by:  elsnd  4600  elsn2g  4623  nelsn  4625  elpwunsn  4643  eqoreldif  4644  disjsn2  4671  rabsnifsb  4681  sssn  4784  disjxsn  5094  opth1  5431  sosn  5719  ressn  6251  elsnxp  6257  elsuci  6394  funcnvsn  6550  funopdmsn  7105  fvconst  7118  fnsnr  7119  fmptap  7126  mposnif  7484  resf1extb  7886  1stconst  8052  2ndconst  8053  reldmtpos  8186  tpostpos  8198  disjen  9074  map2xp  9087  en1eqsn  9187  ac6sfi  9196  ixpfi2  9262  elfi2  9329  fisn  9342  unxpwdom2  9505  cantnfp1lem3  9601  djulf1o  9836  djurf1o  9837  djur  9843  eldju2ndl  9848  eldju2ndr  9849  isfin4p1  10237  dcomex  10369  iundom2g  10462  fpwwe2lem12  10565  canthp1lem2  10576  0tsk  10678  elreal2  11055  ax1rid  11084  ltxrlt  11215  un0addcl  12446  un0mulcl  12447  fzodisjsn  13625  elfzonlteqm1  13669  elfzo0l  13684  elfzr  13709  elfzlmr  13710  seqf1o  13978  seqid3  13981  seqz  13985  1exp  14026  hashnn0pnf  14277  hash1elsn  14306  hashprg  14330  cats1un  14656  fsumss  15660  sumsnf  15678  fsumsplitsn  15679  fsum2dlem  15705  fsumcom2  15709  ackbijnn  15763  fprodss  15883  fprod2dlem  15915  fprodcom2  15919  fprodsplitsn  15924  sumeven  16326  sumodd  16327  divalgmod  16345  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  phi1  16712  dfphi2  16713  nnnn0modprm0  16746  ramubcl  16958  0ram  16960  ramz  16965  imasvscafn  17470  mreexmrid  17578  2initoinv  17946  2termoinv  17953  gsumress  18619  gsumval2  18623  smndex1basss  18842  smndex1mndlem  18846  0nsg  19110  symgextf1lem  19361  symgextf1  19362  pmtrprfval  19428  psgnsn  19461  lsmdisj2  19623  subgdisj1  19632  lt6abl  19836  gsumsnfd  19892  gsumzunsnd  19897  gsumunsnfd  19898  gsum2dlem2  19912  dprdfeq0  19965  dprdsn  19979  dprd2da  19985  pgpfac1lem3a  20019  pgpfaclem2  20025  ablsimpnosubgd  20047  c0snmgmhm  20410  0ring01eq  20474  zrinitorngc  20587  lsssn0  20911  lspsneq0  20975  lspdisjb  21093  pzriprnglem12  21459  frgpcyg  21540  obselocv  21695  obs2ss  21696  mplcoe5  22007  psdmul  22121  coe1tm  22227  mat0dim0  22423  mat0dimid  22424  mat0dimscm  22425  mat1dimscm  22431  mavmul0g  22509  mdet0pr  22548  mdetunilem9  22576  cramer0  22646  pmatcollpw3fi1lem1  22742  basdif0  22909  ordtbas  23148  ordtrest2  23160  cmpfi  23364  refun0  23471  txdis1cn  23591  ptrescn  23595  txkgen  23608  xkoptsub  23610  ordthmeolem  23757  pt1hmeo  23762  filconn  23839  filufint  23876  flimclslem  23940  ptcmplem3  24010  idnghm  24699  iccpnfcnv  24910  iccpnfhmeo  24911  bndth  24925  ivthicc  25427  ovoliunlem1  25471  i1fima2sn  25649  i1f1  25659  itg1addlem4  25668  itg1addlem5  25669  i1fmulc  25672  limcres  25855  limccnp  25860  limccnp2  25861  degltlem1  26045  ply1rem  26139  fta1blem  26144  ig1pdvds  26153  plyeq0lem  26183  plypf1  26185  plyaddlem1  26186  plymullem1  26187  coemulhi  26227  plycj  26251  plycjOLD  26253  taylfval  26334  abelthlem3  26411  rlimcnp  26943  wilthlem2  27047  logexprlim  27204  2sqreultblem  27427  tgldim0eq  28587  edglnl  29228  nbgr1vtx  29443  vtxdginducedm1lem4  29628  clwlkclwwlklem2a4  30084  eucrct2eupth  30332  frgrncvvdeqlem9  30394  nsnlplig  30569  nsnlpligALT  30570  fsumiunle  32921  cshw1s2  33053  gsumhashmul  33161  xrge0tsmsbi  33168  gsumwrd2dccatlem  33171  cyc3evpm  33244  0ringcring  33346  pidlnz  33469  elrspunidl  33521  0ringprmidl  33542  drngmxidlr  33571  ig1pmindeg  33695  mplmulmvr  33716  vieta  33757  lbslsat  33794  lindsunlem  33802  irngnminplynz  33890  ordtrest2NEW  34101  xrge0iifcnv  34111  xrge0iifhom  34115  esumsnf  34242  esumpr  34244  esumiun  34272  inelpisys  34332  measvunilem0  34391  measvuni  34392  carsggect  34496  omsmeas  34501  plymulx0  34725  repr0  34789  bnj98  35043  bnj1442  35225  bnj1452  35228  subfacp1lem5  35400  erdszelem4  35410  erdszelem8  35414  sconnpi1  35455  cvmlift2lem6  35524  cvmlift2lem12  35530  fmla0xp  35599  onint1  36665  bj-1nel0  37202  bj-sngltag  37231  bj-projval  37244  bj-elsn0  37410  bj-fununsn1  37508  tan2h  37863  lindsenlbs  37866  matunitlindf  37869  ptrest  37870  poimirlem23  37894  poimirlem24  37895  poimirlem25  37896  poimirlem28  37899  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  poimirlem32  37903  prdsbnd  38044  rrnequiv  38086  grpokerinj  38144  rngoueqz  38191  gidsn  38203  0rngo  38278  isdmn3  38325  dibelval2nd  41528  hdmaprnlem9N  42233  hdmap14lem4a  42247  dvrelog2b  42436  sticksstones11  42526  unitscyglem2  42566  0prjspnrel  42985  hbtlem5  43485  flcidc  43527  safesnsupfiss  43771  frege133d  44121  radcnvrat  44670  unisnALT  45281  sumsnd  45386  fnchoice  45389  rnsnf  45543  founiiun0  45549  elmapsnd  45562  fsneqrn  45569  infxrpnf  45804  supminfxr2  45827  cncfiooicc  46252  fperdvper  46277  dvmptfprodlem  46302  dvnprodlem1  46304  dvnprodlem2  46305  itgcoscmulx  46327  stoweidlem44  46402  fourierdlem49  46513  fourierdlem56  46520  fourierdlem80  46544  fourierdlem93  46557  fourierdlem101  46565  sge00  46734  sge0sn  46737  sge0snmpt  46741  sge0iunmptlemfi  46771  sge0p1  46772  sge0fodjrnlem  46774  sge0snmptf  46795  sge0splitsn  46799  nnfoctbdjlem  46813  meadjiunlem  46823  ismeannd  46825  caratheodorylem1  46884  isomenndlem  46888  hoidmv1le  46952  hoidmvlelem2  46954  hoidmvlelem3  46955  ovnhoilem1  46959  hoiqssbl  46983  ovnovollem1  47014  ovnovollem2  47015  chnerlem1  47240  eldmressn  47397  iccpartltu  47785  sbgoldbo  48147  nnsum3primesprm  48150  bgoldbtbndlem3  48167  stgr1  48321  gpgprismgr4cycllem7  48461  ldepspr  48833  lmod1zr  48853  termcbas2  49841  idfudiag1  49884