Theorem elsni 4585

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

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

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 4569

This theorem is referenced by:  elsnd  4586  elsn2g  4609  nelsn  4611  elpwunsn  4629  eqoreldif  4630  disjsn2  4657  rabsnifsb  4667  sssn  4770  disjxsn  5080  opth1  5424  sosn  5712  ressn  6244  elsnxp  6250  elsuci  6387  funcnvsn  6543  funopdmsn  7098  fvconst  7111  fnsnr  7112  fmptap  7119  mposnif  7477  resf1extb  7879  1stconst  8044  2ndconst  8045  reldmtpos  8178  tpostpos  8190  disjen  9066  map2xp  9079  en1eqsn  9179  ac6sfi  9188  ixpfi2  9254  elfi2  9321  fisn  9334  unxpwdom2  9497  cantnfp1lem3  9595  djulf1o  9830  djurf1o  9831  djur  9837  eldju2ndl  9842  eldju2ndr  9843  isfin4p1  10231  dcomex  10363  iundom2g  10456  fpwwe2lem12  10559  canthp1lem2  10570  0tsk  10672  elreal2  11049  ax1rid  11078  ltxrlt  11210  un0addcl  12464  un0mulcl  12465  fzodisjsn  13646  elfzonlteqm1  13690  elfzo0l  13705  elfzr  13730  elfzlmr  13731  seqf1o  13999  seqid3  14002  seqz  14006  1exp  14047  hashnn0pnf  14298  hash1elsn  14327  hashprg  14351  cats1un  14677  fsumss  15681  sumsnf  15699  fsumsplitsn  15700  fsum2dlem  15726  fsumcom2  15730  ackbijnn  15787  fprodss  15907  fprod2dlem  15939  fprodcom2  15943  fprodsplitsn  15948  sumeven  16350  sumodd  16351  divalgmod  16369  lcmfunsnlem2lem1  16601  lcmfunsnlem2lem2  16602  phi1  16737  dfphi2  16738  nnnn0modprm0  16771  ramubcl  16983  0ram  16985  ramz  16990  imasvscafn  17495  mreexmrid  17603  2initoinv  17971  2termoinv  17978  gsumress  18644  gsumval2  18648  smndex1basss  18870  smndex1mndlem  18874  0nsg  19138  symgextf1lem  19389  symgextf1  19390  pmtrprfval  19456  psgnsn  19489  lsmdisj2  19651  subgdisj1  19660  lt6abl  19864  gsumsnfd  19920  gsumzunsnd  19925  gsumunsnfd  19926  gsum2dlem2  19940  dprdfeq0  19993  dprdsn  20007  dprd2da  20013  pgpfac1lem3a  20047  pgpfaclem2  20053  ablsimpnosubgd  20075  c0snmgmhm  20436  0ring01eq  20500  zrinitorngc  20613  lsssn0  20937  lspsneq0  21001  lspdisjb  21119  pzriprnglem12  21485  frgpcyg  21566  obselocv  21721  obs2ss  21722  mplcoe5  22031  psdmul  22145  coe1tm  22251  mat0dim0  22445  mat0dimid  22446  mat0dimscm  22447  mat1dimscm  22453  mavmul0g  22531  mdet0pr  22570  mdetunilem9  22598  cramer0  22668  pmatcollpw3fi1lem1  22764  basdif0  22931  ordtbas  23170  ordtrest2  23182  cmpfi  23386  refun0  23493  txdis1cn  23613  ptrescn  23617  txkgen  23630  xkoptsub  23632  ordthmeolem  23779  pt1hmeo  23784  filconn  23861  filufint  23898  flimclslem  23962  ptcmplem3  24032  idnghm  24721  iccpnfcnv  24924  iccpnfhmeo  24925  bndth  24938  ivthicc  25438  ovoliunlem1  25482  i1fima2sn  25660  i1f1  25670  itg1addlem4  25679  itg1addlem5  25680  i1fmulc  25683  limcres  25866  limccnp  25871  limccnp2  25872  degltlem1  26050  ply1rem  26144  fta1blem  26149  ig1pdvds  26158  plyeq0lem  26188  plypf1  26190  plyaddlem1  26191  plymullem1  26192  coemulhi  26232  plycj  26255  plycjOLD  26257  taylfval  26338  abelthlem3  26414  rlimcnp  26945  wilthlem2  27049  logexprlim  27205  2sqreultblem  27428  tgldim0eq  28588  edglnl  29229  nbgr1vtx  29444  vtxdginducedm1lem4  29629  clwlkclwwlklem2a4  30085  eucrct2eupth  30333  frgrncvvdeqlem9  30395  nsnlplig  30570  nsnlpligALT  30571  fsumiunle  32920  cshw1s2  33038  gsumhashmul  33146  xrge0tsmsbi  33153  gsumwrd2dccatlem  33156  cyc3evpm  33229  0ringcring  33331  pidlnz  33454  elrspunidl  33506  0ringprmidl  33527  drngmxidlr  33556  ig1pmindeg  33680  mplmulmvr  33701  vieta  33742  lbslsat  33779  lindsunlem  33787  irngnminplynz  33875  ordtrest2NEW  34086  xrge0iifcnv  34096  xrge0iifhom  34100  esumsnf  34227  esumpr  34229  esumiun  34257  inelpisys  34317  measvunilem0  34376  measvuni  34377  carsggect  34481  omsmeas  34486  plymulx0  34710  repr0  34774  bnj98  35028  bnj1442  35210  bnj1452  35213  subfacp1lem5  35385  erdszelem4  35395  erdszelem8  35399  sconnpi1  35440  cvmlift2lem6  35509  cvmlift2lem12  35515  fmla0xp  35584  onint1  36650  dfttc4lem2  36730  bj-1nel0  37280  bj-sngltag  37309  bj-projval  37322  bj-elsn0  37488  bj-fununsn1  37586  tan2h  37950  lindsenlbs  37953  matunitlindf  37956  ptrest  37957  poimirlem23  37981  poimirlem24  37982  poimirlem25  37983  poimirlem28  37986  poimirlem29  37987  poimirlem30  37988  poimirlem31  37989  poimirlem32  37990  prdsbnd  38131  rrnequiv  38173  grpokerinj  38231  rngoueqz  38278  gidsn  38290  0rngo  38365  isdmn3  38412  dibelval2nd  41615  hdmaprnlem9N  42320  hdmap14lem4a  42334  dvrelog2b  42522  sticksstones11  42612  unitscyglem2  42652  0prjspnrel  43077  hbtlem5  43577  flcidc  43619  safesnsupfiss  43863  frege133d  44213  radcnvrat  44762  unisnALT  45373  sumsnd  45478  fnchoice  45481  rnsnf  45635  founiiun0  45641  elmapsnd  45654  fsneqrn  45661  infxrpnf  45895  supminfxr2  45918  cncfiooicc  46343  fperdvper  46368  dvmptfprodlem  46393  dvnprodlem1  46395  dvnprodlem2  46396  itgcoscmulx  46418  stoweidlem44  46493  fourierdlem49  46604  fourierdlem56  46611  fourierdlem80  46635  fourierdlem93  46648  fourierdlem101  46656  sge00  46825  sge0sn  46828  sge0snmpt  46832  sge0iunmptlemfi  46862  sge0p1  46863  sge0fodjrnlem  46865  sge0snmptf  46886  sge0splitsn  46890  nnfoctbdjlem  46904  meadjiunlem  46914  ismeannd  46916  caratheodorylem1  46975  isomenndlem  46979  hoidmv1le  47043  hoidmvlelem2  47045  hoidmvlelem3  47046  ovnhoilem1  47050  hoiqssbl  47074  ovnovollem1  47105  ovnovollem2  47106  chnerlem1  47331  eldmressn  47500  iccpartltu  47900  sbgoldbo  48278  nnsum3primesprm  48281  bgoldbtbndlem3  48298  stgr1  48452  gpgprismgr4cycllem7  48592  ldepspr  48964  lmod1zr  48984  termcbas2  49972  idfudiag1  50015