Theorem elsni 4599

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-sn 4583

This theorem is referenced by:  elsnd  4600  elsn2g  4623  nelsn  4625  elpwunsn  4643  eqoreldif  4644  disjsn2  4671  rabsnifsb  4681  sssn  4784  disjxsn  5094  opth1  5443  sosn  5734  ressn  6272  elsnxp  6278  elsuci  6415  funcnvsn  6571  funopdmsn  7133  fvconst  7146  fnsnr  7147  fmptap  7154  mposnif  7512  resf1extb  7915  1stconst  8079  2ndconst  8080  reldmtpos  8214  tpostpos  8226  disjen  9106  map2xp  9119  en1eqsn  9219  ac6sfi  9228  ixpfi2  9293  elfi2  9360  fisn  9373  unxpwdom2  9536  cantnfp1lem3  9635  djulf1o  9870  djurf1o  9871  djur  9877  eldju2ndl  9882  eldju2ndr  9883  isfin4p1  10272  dcomex  10404  iundom2g  10497  fpwwe2lem12  10600  canthp1lem2  10611  0tsk  10713  elreal2  11090  ax1rid  11119  ltxrlt  11253  un0addcl  12514  un0mulcl  12515  fzodisjsn  13703  elfzonlteqm1  13747  elfzo0l  13762  elfzr  13787  elfzlmr  13788  seqf1o  14056  seqid3  14059  seqz  14063  1exp  14104  hashnn0pnf  14355  hash1elsn  14384  hashprg  14408  cats1un  14734  fsumss  15752  sumsnf  15770  fsumsplitsn  15771  fsum2dlem  15797  fsumcom2  15801  ackbijnn  15858  fprodss  15978  fprod2dlem  16010  fprodcom2  16014  fprodsplitsn  16019  sumeven  16421  sumodd  16422  divalgmod  16440  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  phi1  16808  dfphi2  16809  nnnn0modprm0  16842  ramubcl  17054  0ram  17056  ramz  17061  imasvscafn  17567  mreexmrid  17675  2initoinv  18043  2termoinv  18050  gsumress  18716  gsumval2  18720  smndex1basss  18942  smndex1mndlem  18946  0nsg  19210  symgextf1lem  19460  symgextf1  19461  pmtrprfval  19527  psgnsn  19560  lsmdisj2  19722  subgdisj1  19731  lt6abl  19935  gsumsnfd  19991  gsumzunsnd  19996  gsumunsnfd  19997  gsum2dlem2  20011  dprdfeq0  20064  dprdsn  20078  dprd2da  20084  pgpfac1lem3a  20118  pgpfaclem2  20124  ablsimpnosubgd  20146  c0snmgmhm  20511  0ring01eq  20579  zrinitorngc  20692  lsssn0  21015  lspsneq0  21079  lspdisjb  21196  pzriprnglem12  21544  frgpcyg  21625  obselocv  21780  obs2ss  21781  mplcoe5  22093  psdmul  22231  coe1tm  22336  mat0dim0  22527  mat0dimid  22528  mat0dimscm  22529  mat1dimscm  22535  mavmul0g  22613  mdet0pr  22652  mdetunilem9  22680  cramer0  22750  pmatcollpw3fi1lem1  22846  basdif0  23013  ordtbas  23252  ordtrest2  23264  cmpfi  23468  refun0  23575  txdis1cn  23695  ptrescn  23699  txkgen  23712  xkoptsub  23714  ordthmeolem  23861  pt1hmeo  23866  filconn  23943  filufint  23980  flimclslem  24044  ptcmplem3  24114  idnghm  24803  iccpnfcnv  25006  iccpnfhmeo  25007  bndth  25020  ivthicc  25520  ovoliunlem1  25564  i1fima2sn  25742  i1f1  25752  itg1addlem4  25761  itg1addlem5  25762  i1fmulc  25765  limcres  25948  limccnp  25953  limccnp2  25954  degltlem1  26132  ply1rem  26226  fta1blem  26231  ig1pdvds  26240  plyeq0lem  26270  plypf1  26272  plyaddlem1  26273  plymullem1  26274  coemulhi  26314  plycj  26337  plycjOLD  26339  plyn0mulidp  26345  taylfval  26422  abelthlem3  26496  rlimcnp  27030  wilthlem2  27133  logexprlim  27289  2sqreultblem  27512  tgldim0eq  28672  edglnl  29344  nbgr1vtx  29559  vtxdginducedm1lem4  29743  clwlkclwwlklem2a4  30199  eucrct2eupth  30447  frgrncvvdeqlem9  30509  nsnlplig  30684  nsnlpligALT  30685  fsumiunle  33031  cshw1s2  33138  gsumhashmul  33247  xrge0tsmsbi  33254  gsumwrd2dccatlem  33257  cyc3evpm  33330  0ringcring  33433  pidlnz  33562  elrspunidl  33614  0ringprmidl  33636  drngmxidlr  33666  ig1pmindeg  33798  0mplrim  33811  selvply1rhmlemb  33816  mplmulmvr  33836  vieta  33877  lbslsat  33913  lindsunlem  33921  irngnminplynz  34009  ordtrest2NEW  34220  xrge0iifcnv  34230  xrge0iifhom  34234  esumsnf  34361  esumpr  34363  esumiun  34391  inelpisys  34451  measvunilem0  34510  measvuni  34511  carsggect  34615  omsmeas  34620  repr0  34905  bnj98  35162  bnj1442  35344  bnj1452  35347  subfacp1lem5  35534  erdszelem4  35544  erdszelem8  35548  sconnpi1  35589  cvmlift2lem6  35658  cvmlift2lem12  35664  fmla0xp  35733  onint1  36809  dfttc4lem2  36889  bj-1nel0  37439  bj-sngltag  37468  bj-projval  37481  bj-elsn0  37647  bj-fununsn1  37745  tan2h  38111  lindsenlbs  38114  matunitlindf  38117  ptrest  38118  poimirlem23  38142  poimirlem24  38143  poimirlem25  38144  poimirlem28  38147  poimirlem29  38148  poimirlem30  38149  poimirlem31  38150  poimirlem32  38151  prdsbnd  38292  rrnequiv  38334  grpokerinj  38392  rngoueqz  38439  gidsn  38451  0rngo  38526  isdmn3  38573  dibelval2nd  41776  hdmaprnlem9N  42481  hdmap14lem4a  42495  dvrelog2b  42683  sticksstones11  42773  unitscyglem2  42813  0prjspnrel  43209  hbtlem5  43705  flcidc  43747  safesnsupfiss  43991  frege133d  44341  radcnvrat  44890  unisnALT  45501  sumsnd  45606  fnchoice  45609  rnsnf  45762  founiiun0  45768  elmapsnd  45781  fsneqrn  45787  infxrpnf  46020  supminfxr2  46043  cncfiooicc  46468  fperdvper  46493  dvmptfprodlem  46518  dvnprodlem1  46520  dvnprodlem2  46521  itgcoscmulx  46543  stoweidlem44  46618  fourierdlem49  46729  fourierdlem56  46736  fourierdlem80  46760  fourierdlem93  46773  fourierdlem101  46781  sge00  46950  sge0sn  46953  sge0snmpt  46957  sge0iunmptlemfi  46987  sge0p1  46988  sge0fodjrnlem  46990  sge0snmptf  47011  sge0splitsn  47015  nnfoctbdjlem  47029  meadjiunlem  47039  ismeannd  47041  caratheodorylem1  47100  isomenndlem  47104  hoidmv1le  47168  hoidmvlelem2  47170  hoidmvlelem3  47171  ovnhoilem1  47175  hoiqssbl  47199  ovnovollem1  47230  ovnovollem2  47231  chnerlem1  47458  eldmressn  47631  iccpartltu  48031  sbgoldbo  48409  nnsum3primesprm  48412  bgoldbtbndlem3  48429  stgr1  48583  gpgprismgr4cycllem7  48723  ldepspr  49095  lmod1zr  49115  termcbas2  50103  idfudiag1  50146