Theorem elsni 4601

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sn 4589

This theorem is used by:  elsnd  4602  elsn2g  4626  nelsn  4628  elpwunsn  4646  eqoreldif  4647  disjsn2  4674  rabsnifsb  4685  sssn  4787  disjxsn  5102  opth1  5451  sosn  5746  ressn  6312  elsnxp  6320  elsuci  6458  funcnvsn  6620  funopdmsn  7186  fvconst  7199  fnsnr  7200  fmptap  7206  mposnif  7567  resf1extb  7980  1stconst  8148  2ndconst  8149  reldmtpos  8289  tpostpos  8301  disjen  9191  map2xp  9204  en1eqsn  9304  ac6sfi  9313  ixpfi2  9377  elfi2  9443  fisn  9456  unxpwdom2  9619  cantnfp1lem3  9718  djulf1o  10030  djurf1o  10031  djur  10037  eldju2ndl  10042  eldju2ndr  10043  isfin4p1  10432  dcomex  10564  iundom2g  10663  fpwwe2lem12  10766  canthp1lem2  10777  0tsk  10879  elreal2  11256  ax1rid  11285  ltxrlt  11419  un0addcl  12679  un0mulcl  12680  fzodisjsn  13872  elfzonlteqm1  13916  elfzo0l  13931  elfzr  13956  elfzlmr  13957  seqf1o  14226  seqid3  14229  seqz  14233  1exp  14274  hashnn0pnf  14527  hash1elsn  14556  hashprg  14580  cats1un  14912  fsumss  15935  sumsnf  15953  fsumsplitsn  15954  fsum2dlem  15980  fsumcom2  15984  ackbijnn  16041  fprodss  16159  fprod2dlem  16191  fprodcom2  16195  fprodsplitsn  16200  sumeven  16601  sumodd  16602  divalgmod  16620  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  phi1  16994  dfphi2  16995  nnnn0modprm0  17028  ramubcl  17240  0ram  17242  ramz  17247  imasvscafn  17759  mreexmrid  17867  2initoinv  18235  2termoinv  18242  gsumress  18921  gsumval2  18925  smndex1basss  19154  smndex1mndlem  19158  0nsg  19429  symgextf1lem  19685  symgextf1  19686  pmtrprfval  19752  psgnsn  19785  lsmdisj2  19947  subgdisj1  19956  lt6abl  20160  gsumsnfd  20216  gsumzunsnd  20221  gsumunsnfd  20222  gsum2dlem2  20236  dprdfeq0  20289  dprdsn  20303  dprd2da  20309  pgpfac1lem3a  20343  pgpfaclem2  20349  ablsimpnosubgd  20371  c0snmgmhm  20743  0ring01eq  20831  zrinitorngc  20945  lsssn0  21274  lspsneq0  21338  lspdisjb  21455  pidlnz  21579  0ringprmidl  21684  pzriprnglem12  21853  frgpcyg  21934  obselocv  22089  obs2ss  22090  lindsenlbs  22212  mplcoe5  22404  psdmul  22542  coe1tm  22647  mat0dim0  22837  mat0dimid  22838  mat0dimscm  22839  mat1dimscm  22845  mavmul0g  22923  mdet0pr  22962  mdetunilem9  22990  matunitlindf  23051  cramer0  23063  pmatcollpw3fi1lem1  23159  basdif0  23326  ordtbas  23565  ordtrest2  23577  cmpfi  23781  refun0  23889  txdis1cn  24009  ptrescn  24013  txkgen  24026  xkoptsub  24028  ordthmeolem  24175  pt1hmeo  24180  filconn  24257  filufint  24294  flimclslem  24358  ptcmplem3  24428  idnghm  25117  iccpnfcnv  25320  iccpnfhmeo  25321  bndth  25334  ivthicc  25834  ovoliunlem1  25878  i1fima2sn  26056  i1f1  26066  itg1addlem4  26075  itg1addlem5  26076  i1fmulc  26079  limcres  26261  limccnp  26266  limccnp2  26267  degltlem1  26445  ply1rem  26539  fta1blem  26544  ig1pdvds  26553  plyeq0lem  26584  plypf1  26586  plyaddlem1  26587  plymullem1  26588  coemulhi  26628  plycj  26651  plyn0mulidp  26657  taylfval  26743  abelthlem3  26817  rlimcnp  27350  wilthlem2  27453  logexprlim  27609  2sqreultblem  27832  tgldim0eq  29023  edglnl  29778  nbgr1vtx  29996  vtxdginducedm1lem4  30180  clwlkclwwlklem2a4  30645  eucrct2eupth  30903  frgrncvvdeqlem9  30965  nsnlplig  31140  nsnlpligALT  31141  fsumiunle  33516  cshw1s2  33617  gsumhashmul  33727  xrge0tsmsbi  33734  gsumwrd2dccatlem  33737  cyc3evpm  33810  0ringcring  33912  elrspunidl  34082  drngmxidlr  34106  ig1pmindeg  34237  0mplrim  34257  selvply1rhmlemb  34262  mplmulmvr  34282  vieta  34323  lbslsat  34359  lindsunlem  34367  irngnminplynz  34455  ordtrest2NEW  34666  xrge0iifcnv  34676  xrge0iifhom  34680  esumsnf  34807  esumpr  34809  esumiun  34837  inelpisys  34898  measvunilem0  34957  measvuni  34958  carsggect  35061  omsmeas  35066  repr0  35351  bnj98  35608  bnj1442  35790  bnj1452  35793  subfacp1lem5  36157  erdszelem4  36167  erdszelem8  36171  sconnpi1  36212  cvmlift2lem6  36281  cvmlift2lem12  36287  fmla0xp  36356  onint1  37452  dfttc4lem2  37532  bj-1nel0  38082  bj-sngltag  38111  bj-projval  38124  bj-elsn0  38344  bj-fununsn1  38442  tan2h  38803  ptrest  38805  poimirlem23  38829  poimirlem24  38830  poimirlem25  38831  poimirlem28  38834  poimirlem29  38835  poimirlem30  38836  poimirlem31  38837  poimirlem32  38838  prdsbnd  38993  rrnequiv  39035  grpokerinj  39093  rngoueqz  39140  gidsn  39152  0rngo  39227  isdmn3  39274  dibelval2nd  42475  hdmaprnlem9N  43180  hdmap14lem4a  43194  dvrelog2b  43382  sticksstones11  43472  unitscyglem2  43512  0prjspnrel  43929  hbtlem5  44395  flcidc  44433  safesnsupfiss  44677  frege133d  45026  radcnvrat  45559  unisnALT  46168  sumsnd  46317  fnchoice  46320  rnsnf  46472  founiiun0  46478  elmapsnd  46491  fsneqrn  46497  infxrpnf  46729  supminfxr2  46752  cncfiooicc  47177  fperdvper  47202  dvmptfprodlem  47227  dvnprodlem1  47229  dvnprodlem2  47230  itgcoscmulx  47252  stoweidlem44  47327  fourierdlem49  47438  fourierdlem56  47445  fourierdlem80  47469  fourierdlem93  47482  fourierdlem101  47490  sge00  47659  sge0sn  47662  sge0snmpt  47666  sge0iunmptlemfi  47696  sge0p1  47697  sge0fodjrnlem  47699  sge0snmptf  47720  sge0splitsn  47724  nnfoctbdjlem  47738  meadjiunlem  47748  ismeannd  47750  caratheodorylem1  47809  isomenndlem  47813  hoidmv1le  47877  hoidmvlelem2  47879  hoidmvlelem3  47880  ovnhoilem1  47884  hoiqssbl  47908  ovnovollem1  47939  ovnovollem2  47940  eldmressn  48380  iccpartltu  48780  sbgoldbo  49158  nnsum3primesprm  49161  bgoldbtbndlem3  49178  stgr1  49332  gpgprismgr4cycllem7  49472  isidom3  49773  ldepspr  49916  lmod1zr  49936  termcbas2  50948  idfudiag1  50991