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  32774  cshw1s2  32902  gsumhashmul  33014  xrge0tsmsbi  33016  gsumwrd2dccatlem  33019  cyc3evpm  33092  0ringcring  33192  pidlnz  33313  elrspunidl  33365  0ringprmidl  33386  drngmxidlr  33415  ig1pmindeg  33534  lbslsat  33583  lindsunlem  33591  irngnminplynz  33679  ordtrest2NEW  33890  xrge0iifcnv  33900  xrge0iifhom  33904  esumsnf  34031  esumpr  34033  esumiun  34061  inelpisys  34121  measvunilem0  34180  measvuni  34181  carsggect  34286  omsmeas  34291  plymulx0  34515  repr0  34579  bnj98  34834  bnj1442  35016  bnj1452  35019  subfacp1lem5  35161  erdszelem4  35171  erdszelem8  35175  sconnpi1  35216  cvmlift2lem6  35285  cvmlift2lem12  35291  fmla0xp  35360  onint1  36427  bj-1nel0  36932  bj-sngltag  36961  bj-projval  36974  bj-elsn0  37133  bj-fununsn1  37231  tan2h  37596  lindsenlbs  37599  matunitlindf  37602  ptrest  37603  poimirlem23  37627  poimirlem24  37628  poimirlem25  37629  poimirlem28  37632  poimirlem29  37633  poimirlem30  37634  poimirlem31  37635  poimirlem32  37636  prdsbnd  37777  rrnequiv  37819  grpokerinj  37877  rngoueqz  37924  gidsn  37936  0rngo  38011  isdmn3  38058  dibelval2nd  41135  hdmaprnlem9N  41840  hdmap14lem4a  41854  dvrelog2b  42043  sticksstones11  42133  unitscyglem2  42173  0prjspnrel  42604  hbtlem5  43105  flcidc  43147  safesnsupfiss  43392  frege133d  43742  radcnvrat  44291  unisnALT  44903  sumsnd  45008  fnchoice  45011  rnsnf  45166  founiiun0  45172  elmapsnd  45186  fsneqrn  45193  infxrpnf  45429  supminfxr2  45452  cncfiooicc  45879  fperdvper  45904  dvmptfprodlem  45929  dvnprodlem1  45931  dvnprodlem2  45932  itgcoscmulx  45954  stoweidlem44  46029  fourierdlem49  46140  fourierdlem56  46147  fourierdlem80  46171  fourierdlem93  46184  fourierdlem101  46192  sge00  46361  sge0sn  46364  sge0snmpt  46368  sge0iunmptlemfi  46398  sge0p1  46399  sge0fodjrnlem  46401  sge0snmptf  46422  sge0splitsn  46426  nnfoctbdjlem  46440  meadjiunlem  46450  ismeannd  46452  caratheodorylem1  46511  isomenndlem  46515  hoidmv1le  46579  hoidmvlelem2  46581  hoidmvlelem3  46582  ovnhoilem1  46586  hoiqssbl  46610  ovnovollem1  46641  ovnovollem2  46642  eldmressn  47025  iccpartltu  47413  sbgoldbo  47775  nnsum3primesprm  47778  bgoldbtbndlem3  47795  stgr1  47949  gpgprismgr4cycllem7  48089  ldepspr  48462  lmod1zr  48482  termcbas2  49471  idfudiag1  49514