Theorem elsni 4611

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sn 4595

This theorem is referenced by:  elsnd  4612  elsn2g  4635  nelsn  4637  elpwunsn  4655  eqoreldif  4656  disjsn2  4683  rabsnifsb  4693  sssn  4796  disjxsn  5107  opth1  5458  sosn  5749  ressn  6287  elsnxp  6293  elsuci  6431  funcnvsn  6587  funopdmsn  7148  fvconst  7161  fnsnr  7162  fmptap  7169  mposnif  7527  resf1extb  7930  1stconst  8094  2ndconst  8095  reldmtpos  8229  tpostpos  8241  disjen  9121  map2xp  9134  en1eqsn  9234  ac6sfi  9243  ixpfi2  9306  elfi2  9373  fisn  9386  unxpwdom2  9549  cantnfp1lem3  9648  djulf1o  9897  djurf1o  9898  djur  9904  eldju2ndl  9909  eldju2ndr  9910  isfin4p1  10298  dcomex  10430  iundom2g  10523  fpwwe2lem12  10626  canthp1lem2  10637  0tsk  10739  elreal2  11116  ax1rid  11145  ltxrlt  11279  un0addcl  12536  un0mulcl  12537  fzodisjsn  13725  elfzonlteqm1  13769  elfzo0l  13784  elfzr  13809  elfzlmr  13810  seqf1o  14078  seqid3  14081  seqz  14085  1exp  14126  hashnn0pnf  14377  hash1elsn  14406  hashprg  14430  cats1un  14757  fsumss  15775  sumsnf  15793  fsumsplitsn  15794  fsum2dlem  15820  fsumcom2  15824  ackbijnn  15881  fprodss  16001  fprod2dlem  16033  fprodcom2  16037  fprodsplitsn  16042  sumeven  16444  sumodd  16445  divalgmod  16463  lcmfunsnlem2lem1  16695  lcmfunsnlem2lem2  16696  phi1  16831  dfphi2  16832  nnnn0modprm0  16865  ramubcl  17077  0ram  17079  ramz  17084  imasvscafn  17590  mreexmrid  17698  2initoinv  18066  2termoinv  18073  gsumress  18739  gsumval2  18743  smndex1basss  18966  smndex1mndlem  18970  0nsg  19234  symgextf1lem  19489  symgextf1  19490  pmtrprfval  19556  psgnsn  19589  lsmdisj2  19751  subgdisj1  19760  lt6abl  19964  gsumsnfd  20020  gsumzunsnd  20025  gsumunsnfd  20026  gsum2dlem2  20040  dprdfeq0  20093  dprdsn  20107  dprd2da  20113  pgpfac1lem3a  20147  pgpfaclem2  20153  ablsimpnosubgd  20175  c0snmgmhm  20543  0ring01eq  20612  zrinitorngc  20726  lsssn0  21046  lspsneq0  21110  lspdisjb  21227  0ringprmidl  21445  pzriprnglem12  21610  frgpcyg  21691  obselocv  21846  obs2ss  21847  mplcoe5  22159  psdmul  22297  coe1tm  22402  mat0dim0  22592  mat0dimid  22593  mat0dimscm  22594  mat1dimscm  22600  mavmul0g  22678  mdet0pr  22717  mdetunilem9  22745  cramer0  22815  pmatcollpw3fi1lem1  22911  basdif0  23078  ordtbas  23317  ordtrest2  23329  cmpfi  23533  refun0  23640  txdis1cn  23760  ptrescn  23764  txkgen  23777  xkoptsub  23779  ordthmeolem  23926  pt1hmeo  23931  filconn  24008  filufint  24045  flimclslem  24109  ptcmplem3  24179  idnghm  24868  iccpnfcnv  25071  iccpnfhmeo  25072  bndth  25085  ivthicc  25585  ovoliunlem1  25629  i1fima2sn  25807  i1f1  25817  itg1addlem4  25826  itg1addlem5  25827  i1fmulc  25830  limcres  26013  limccnp  26018  limccnp2  26019  degltlem1  26197  ply1rem  26291  fta1blem  26296  ig1pdvds  26305  plyeq0lem  26335  plypf1  26337  plyaddlem1  26338  plymullem1  26339  coemulhi  26379  plycj  26402  plycjOLD  26404  plyn0mulidp  26410  taylfval  26487  abelthlem3  26561  rlimcnp  27095  wilthlem2  27198  logexprlim  27354  2sqreultblem  27577  tgldim0eq  28737  edglnl  29433  nbgr1vtx  29648  vtxdginducedm1lem4  29832  clwlkclwwlklem2a4  30288  eucrct2eupth  30536  frgrncvvdeqlem9  30598  nsnlplig  30773  nsnlpligALT  30774  fsumiunle  33113  cshw1s2  33220  gsumhashmul  33327  xrge0tsmsbi  33334  gsumwrd2dccatlem  33337  cyc3evpm  33410  0ringcring  33512  pidlnz  33632  elrspunidl  33679  drngmxidlr  33704  ig1pmindeg  33836  0mplrim  33848  selvply1rhmlemb  33853  mplmulmvr  33873  vieta  33914  lbslsat  33950  lindsunlem  33958  irngnminplynz  34046  ordtrest2NEW  34257  xrge0iifcnv  34267  xrge0iifhom  34271  esumsnf  34398  esumpr  34400  esumiun  34428  inelpisys  34488  measvunilem0  34547  measvuni  34548  carsggect  34652  omsmeas  34657  repr0  34942  bnj98  35199  bnj1442  35381  bnj1452  35384  subfacp1lem5  35574  erdszelem4  35584  erdszelem8  35588  sconnpi1  35629  cvmlift2lem6  35698  cvmlift2lem12  35704  fmla0xp  35773  onint1  36848  dfttc4lem2  36928  bj-1nel0  37477  bj-sngltag  37506  bj-projval  37519  bj-elsn0  37686  bj-fununsn1  37784  tan2h  38150  lindsenlbs  38153  matunitlindf  38156  ptrest  38157  poimirlem23  38181  poimirlem24  38182  poimirlem25  38183  poimirlem28  38186  poimirlem29  38187  poimirlem30  38188  poimirlem31  38189  poimirlem32  38190  prdsbnd  38331  rrnequiv  38373  grpokerinj  38431  rngoueqz  38478  gidsn  38490  0rngo  38565  isdmn3  38612  dibelval2nd  41815  hdmaprnlem9N  42520  hdmap14lem4a  42534  dvrelog2b  42722  sticksstones11  42812  unitscyglem2  42852  0prjspnrel  43250  hbtlem5  43746  flcidc  43788  safesnsupfiss  44032  frege133d  44382  radcnvrat  44915  unisnALT  45525  sumsnd  45637  fnchoice  45640  rnsnf  45793  founiiun0  45799  elmapsnd  45812  fsneqrn  45818  infxrpnf  46051  supminfxr2  46074  cncfiooicc  46499  fperdvper  46524  dvmptfprodlem  46549  dvnprodlem1  46551  dvnprodlem2  46552  itgcoscmulx  46574  stoweidlem44  46649  fourierdlem49  46760  fourierdlem56  46767  fourierdlem80  46791  fourierdlem93  46804  fourierdlem101  46812  sge00  46981  sge0sn  46984  sge0snmpt  46988  sge0iunmptlemfi  47018  sge0p1  47019  sge0fodjrnlem  47021  sge0snmptf  47042  sge0splitsn  47046  nnfoctbdjlem  47060  meadjiunlem  47070  ismeannd  47072  caratheodorylem1  47131  isomenndlem  47135  hoidmv1le  47199  hoidmvlelem2  47201  hoidmvlelem3  47202  ovnhoilem1  47206  hoiqssbl  47230  ovnovollem1  47261  ovnovollem2  47262  chnerlem1  47489  eldmressn  47662  iccpartltu  48062  sbgoldbo  48440  nnsum3primesprm  48443  bgoldbtbndlem3  48460  stgr1  48614  gpgprismgr4cycllem7  48754  ldepspr  49137  lmod1zr  49157  termcbas2  50144  idfudiag1  50187