Theorem elsni 4597

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4585

This theorem is used by:  elsnd  4598  elsn2g  4621  nelsn  4623  elpwunsn  4641  eqoreldif  4642  disjsn2  4669  rabsnifsb  4679  sssn  4781  disjxsn  5096  opth1  5444  sosn  5739  ressn  6291  elsnxp  6297  elsuci  6435  funcnvsn  6595  funopdmsn  7159  fvconst  7172  fnsnr  7173  fmptap  7179  mposnif  7540  resf1extb  7950  1stconst  8118  2ndconst  8119  reldmtpos  8259  tpostpos  8271  disjen  9161  map2xp  9174  en1eqsn  9274  ac6sfi  9283  ixpfi2  9347  elfi2  9413  fisn  9426  unxpwdom2  9589  cantnfp1lem3  9688  djulf1o  10000  djurf1o  10001  djur  10007  eldju2ndl  10012  eldju2ndr  10013  isfin4p1  10400  dcomex  10532  iundom2g  10631  fpwwe2lem12  10734  canthp1lem2  10745  0tsk  10847  elreal2  11224  ax1rid  11253  ltxrlt  11387  un0addcl  12646  un0mulcl  12647  fzodisjsn  13839  elfzonlteqm1  13883  elfzo0l  13898  elfzr  13923  elfzlmr  13924  seqf1o  14193  seqid3  14196  seqz  14200  1exp  14241  hashnn0pnf  14493  hash1elsn  14522  hashprg  14546  cats1un  14878  fsumss  15900  sumsnf  15918  fsumsplitsn  15919  fsum2dlem  15945  fsumcom2  15949  ackbijnn  16006  fprodss  16124  fprod2dlem  16156  fprodcom2  16160  fprodsplitsn  16165  sumeven  16566  sumodd  16567  divalgmod  16585  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  phi1  16959  dfphi2  16960  nnnn0modprm0  16993  ramubcl  17205  0ram  17207  ramz  17212  imasvscafn  17718  mreexmrid  17826  2initoinv  18194  2termoinv  18201  gsumress  18880  gsumval2  18884  smndex1basss  19113  smndex1mndlem  19117  0nsg  19388  symgextf1lem  19643  symgextf1  19644  pmtrprfval  19710  psgnsn  19743  lsmdisj2  19905  subgdisj1  19914  lt6abl  20118  gsumsnfd  20174  gsumzunsnd  20179  gsumunsnfd  20180  gsum2dlem2  20194  dprdfeq0  20247  dprdsn  20261  dprd2da  20267  pgpfac1lem3a  20301  pgpfaclem2  20307  ablsimpnosubgd  20329  c0snmgmhm  20701  0ring01eq  20789  zrinitorngc  20903  lsssn0  21232  lspsneq0  21296  lspdisjb  21413  pidlnz  21537  0ringprmidl  21642  pzriprnglem12  21807  frgpcyg  21888  obselocv  22043  obs2ss  22044  lindsenlbs  22166  mplcoe5  22358  psdmul  22496  coe1tm  22601  mat0dim0  22791  mat0dimid  22792  mat0dimscm  22793  mat1dimscm  22799  mavmul0g  22877  mdet0pr  22916  mdetunilem9  22944  matunitlindf  23005  cramer0  23017  pmatcollpw3fi1lem1  23113  basdif0  23280  ordtbas  23519  ordtrest2  23531  cmpfi  23735  refun0  23843  txdis1cn  23963  ptrescn  23967  txkgen  23980  xkoptsub  23982  ordthmeolem  24129  pt1hmeo  24134  filconn  24211  filufint  24248  flimclslem  24312  ptcmplem3  24382  idnghm  25071  iccpnfcnv  25274  iccpnfhmeo  25275  bndth  25288  ivthicc  25788  ovoliunlem1  25832  i1fima2sn  26010  i1f1  26020  itg1addlem4  26029  itg1addlem5  26030  i1fmulc  26033  limcres  26215  limccnp  26220  limccnp2  26221  degltlem1  26399  ply1rem  26493  fta1blem  26498  ig1pdvds  26507  plyeq0lem  26538  plypf1  26540  plyaddlem1  26541  plymullem1  26542  coemulhi  26582  plycj  26605  plyn0mulidp  26611  taylfval  26695  abelthlem3  26769  rlimcnp  27302  wilthlem2  27405  logexprlim  27561  2sqreultblem  27784  tgldim0eq  28975  edglnl  29730  nbgr1vtx  29948  vtxdginducedm1lem4  30132  clwlkclwwlklem2a4  30597  eucrct2eupth  30855  frgrncvvdeqlem9  30917  nsnlplig  31092  nsnlpligALT  31093  fsumiunle  33470  cshw1s2  33571  gsumhashmul  33678  xrge0tsmsbi  33685  gsumwrd2dccatlem  33688  cyc3evpm  33761  0ringcring  33863  elrspunidl  34028  drngmxidlr  34052  ig1pmindeg  34184  0mplrim  34196  selvply1rhmlemb  34201  mplmulmvr  34221  vieta  34262  lbslsat  34298  lindsunlem  34306  irngnminplynz  34394  ordtrest2NEW  34605  xrge0iifcnv  34615  xrge0iifhom  34619  esumsnf  34746  esumpr  34748  esumiun  34776  inelpisys  34837  measvunilem0  34896  measvuni  34897  carsggect  35000  omsmeas  35005  repr0  35290  bnj98  35547  bnj1442  35729  bnj1452  35732  subfacp1lem5  36067  erdszelem4  36077  erdszelem8  36081  sconnpi1  36122  cvmlift2lem6  36191  cvmlift2lem12  36197  fmla0xp  36266  onint1  37361  dfttc4lem2  37441  bj-1nel0  37991  bj-sngltag  38020  bj-projval  38033  bj-elsn0  38213  bj-fununsn1  38311  tan2h  38672  ptrest  38674  poimirlem23  38698  poimirlem24  38699  poimirlem25  38700  poimirlem28  38703  poimirlem29  38704  poimirlem30  38705  poimirlem31  38706  poimirlem32  38707  prdsbnd  38864  rrnequiv  38906  grpokerinj  38964  rngoueqz  39011  gidsn  39023  0rngo  39098  isdmn3  39145  dibelval2nd  42346  hdmaprnlem9N  43051  hdmap14lem4a  43065  dvrelog2b  43253  sticksstones11  43343  unitscyglem2  43383  0prjspnrel  43800  hbtlem5  44267  flcidc  44309  safesnsupfiss  44553  frege133d  44902  radcnvrat  45435  unisnALT  46044  sumsnd  46179  fnchoice  46182  rnsnf  46335  founiiun0  46341  elmapsnd  46354  fsneqrn  46360  infxrpnf  46592  supminfxr2  46615  cncfiooicc  47040  fperdvper  47065  dvmptfprodlem  47090  dvnprodlem1  47092  dvnprodlem2  47093  itgcoscmulx  47115  stoweidlem44  47190  fourierdlem49  47301  fourierdlem56  47308  fourierdlem80  47332  fourierdlem93  47345  fourierdlem101  47353  sge00  47522  sge0sn  47525  sge0snmpt  47529  sge0iunmptlemfi  47559  sge0p1  47560  sge0fodjrnlem  47562  sge0snmptf  47583  sge0splitsn  47587  nnfoctbdjlem  47601  meadjiunlem  47611  ismeannd  47613  caratheodorylem1  47672  isomenndlem  47676  hoidmv1le  47740  hoidmvlelem2  47742  hoidmvlelem3  47743  ovnhoilem1  47747  hoiqssbl  47771  ovnovollem1  47802  ovnovollem2  47803  eldmressn  48243  iccpartltu  48643  sbgoldbo  49021  nnsum3primesprm  49024  bgoldbtbndlem3  49041  stgr1  49195  gpgprismgr4cycllem7  49335  isidom3  49578  ldepspr  49721  lmod1zr  49741  termcbas2  50753  idfudiag1  50796