Theorem elsni 4542

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sn 4526

This theorem is referenced by:  elsn2g  4563  nelsn  4565  elpwunsn  4581  eqoreldif  4582  disjsn2  4608  rabsnifsb  4618  sssn  4719  disjxsn  5023  opth1  5332  sosn  5602  ressn  6104  elsnxp  6110  elsuci  6225  funcnvsn  6374  funopdmsn  6889  fvconst  6903  fnsnr  6904  fmptap  6909  mposnif  7247  1stconst  7778  2ndconst  7779  reldmtpos  7883  tpostpos  7895  disjen  8658  map2xp  8671  ac6sfi  8746  ixpfi2  8806  elfi2  8862  fisn  8875  unxpwdom2  9036  cantnfp1lem3  9127  djulf1o  9325  djurf1o  9326  djur  9332  eldju2ndl  9337  eldju2ndr  9338  isfin4p1  9726  dcomex  9858  iundom2g  9951  fpwwe2lem13  10053  canthp1lem2  10064  0tsk  10166  elreal2  10543  ax1rid  10572  ltxrlt  10700  un0addcl  11918  un0mulcl  11919  fzodisjsn  13070  elfzonlteqm1  13108  elfzo0l  13122  elfzr  13145  elfzlmr  13146  seqf1o  13407  seqid3  13410  seqz  13414  1exp  13454  hashnn0pnf  13698  hash1elsn  13728  hashprg  13752  cats1un  14074  fsumss  15074  sumsnf  15091  fsumsplitsn  15092  fsum2dlem  15117  fsumcom2  15121  ackbijnn  15175  fprodss  15294  fprod2dlem  15326  fprodcom2  15330  fprodsplitsn  15335  sumeven  15728  sumodd  15729  divalgmod  15747  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  phi1  16100  dfphi2  16101  nnnn0modprm0  16133  ramubcl  16344  0ram  16346  ramz  16351  imasvscafn  16802  mreexmrid  16906  2initoinv  17262  2termoinv  17269  gsumress  17884  gsumval2  17888  smndex1basss  18062  smndex1mndlem  18066  0nsg  18313  symgextf1lem  18540  symgextf1  18541  pmtrprfval  18607  psgnsn  18640  lsmdisj2  18800  subgdisj1  18809  lt6abl  19008  gsumsnfd  19064  gsumzunsnd  19069  gsumunsnfd  19070  gsum2dlem2  19084  dprdfeq0  19137  dprdsn  19151  dprd2da  19157  pgpfac1lem3a  19191  pgpfaclem2  19197  ablsimpnosubgd  19219  lsssn0  19712  lspsneq0  19777  lspdisjb  19891  0ring01eq  20037  frgpcyg  20265  obselocv  20417  obs2ss  20418  mplcoe5  20708  coe1tm  20902  mat0dim0  21072  mat0dimid  21073  mat0dimscm  21074  mat1dimscm  21080  mavmul0g  21158  mdet0pr  21197  mdetunilem9  21225  cramer0  21295  pmatcollpw3fi1lem1  21391  basdif0  21558  ordtbas  21797  ordtrest2  21809  cmpfi  22013  refun0  22120  txdis1cn  22240  ptrescn  22244  txkgen  22257  xkoptsub  22259  ordthmeolem  22406  pt1hmeo  22411  filconn  22488  filufint  22525  flimclslem  22589  ptcmplem3  22659  idnghm  23349  iccpnfcnv  23549  iccpnfhmeo  23550  bndth  23563  ivthicc  24062  ovoliunlem1  24106  i1fima2sn  24284  i1f1  24294  itg1addlem4  24303  itg1addlem5  24304  i1fmulc  24307  limcres  24489  limccnp  24494  limccnp2  24495  degltlem1  24673  ply1rem  24764  fta1blem  24769  ig1pdvds  24777  plyeq0lem  24807  plypf1  24809  plyaddlem1  24810  plymullem1  24811  coemulhi  24851  plycj  24874  taylfval  24954  abelthlem3  25028  rlimcnp  25551  wilthlem2  25654  logexprlim  25809  2sqreultblem  26032  tgldim0eq  26297  edglnl  26936  nbgr1vtx  27148  vtxdginducedm1lem4  27332  clwlkclwwlklem2a4  27782  eucrct2eupth  28030  frgrncvvdeqlem9  28092  nsnlplig  28264  nsnlpligALT  28265  fsumiunle  30571  cshw1s2  30660  gsumhashmul  30741  xrge0tsmsbi  30743  cyc3evpm  30842  pidlnz  30991  elrspunidl  31014  0ringprmidl  31033  lbslsat  31102  lindsunlem  31108  ordtrest2NEW  31276  xrge0iifcnv  31286  xrge0iifhom  31290  esumsnf  31433  esumpr  31435  esumiun  31463  inelpisys  31523  measvunilem0  31582  measvuni  31583  carsggect  31686  omsmeas  31691  plymulx0  31927  repr0  31992  bnj98  32249  bnj1442  32431  bnj1452  32434  subfacp1lem5  32544  erdszelem4  32554  erdszelem8  32558  sconnpi1  32599  cvmlift2lem6  32668  cvmlift2lem12  32674  fmla0xp  32743  onint1  33910  bj-1nel0  34390  bj-sngltag  34419  bj-projval  34432  bj-elsn0  34570  bj-fununsn1  34668  bj-isrvec  34708  tan2h  35049  lindsenlbs  35052  matunitlindf  35055  ptrest  35056  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem28  35085  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  prdsbnd  35231  rrnequiv  35273  grpokerinj  35331  rngoueqz  35378  gidsn  35390  0rngo  35465  isdmn3  35512  dibelval2nd  38448  hdmaprnlem9N  39153  hdmap14lem4a  39167  0prjspnrel  39613  hbtlem5  40072  flcidc  40118  frege133d  40466  radcnvrat  41018  unisnALT  41632  sumsnd  41655  fnchoice  41658  rnsnf  41810  founiiun0  41817  elmapsnd  41833  fsneqrn  41840  infxrpnf  42084  supminfxr2  42108  cncfiooicc  42536  fperdvper  42561  dvmptfprodlem  42586  dvnprodlem1  42588  dvnprodlem2  42589  itgcoscmulx  42611  stoweidlem44  42686  fourierdlem49  42797  fourierdlem56  42804  fourierdlem80  42828  fourierdlem93  42841  fourierdlem101  42849  sge00  43015  sge0sn  43018  sge0snmpt  43022  sge0iunmptlemfi  43052  sge0p1  43053  sge0fodjrnlem  43055  sge0snmptf  43076  sge0splitsn  43080  nnfoctbdjlem  43094  meadjiunlem  43104  ismeannd  43106  caratheodorylem1  43165  isomenndlem  43169  hoidmv1le  43233  hoidmvlelem2  43235  hoidmvlelem3  43236  ovnhoilem1  43240  hoiqssbl  43264  ovnovollem1  43295  ovnovollem2  43296  eldmressn  43629  iccpartltu  43942  sbgoldbo  44305  nnsum3primesprm  44308  bgoldbtbndlem3  44325  c0snmgmhm  44538  zrinitorngc  44624  ldepspr  44882  lmod1zr  44902