Theorem elsni 4606

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sn 4590

This theorem is referenced by:  elsnd  4607  elsn2g  4630  nelsn  4632  elpwunsn  4650  eqoreldif  4651  disjsn2  4678  rabsnifsb  4688  sssn  4792  disjxsn  5103  opth1  5457  sosn  5748  ressn  6286  elsnxp  6292  elsuci  6430  funcnvsn  6586  funopdmsn  7147  fvconst  7160  fnsnr  7161  fmptap  7168  mposnif  7526  resf1extb  7927  1stconst  8091  2ndconst  8092  reldmtpos  8226  tpostpos  8238  disjen  9118  map2xp  9131  en1eqsn  9231  ac6sfi  9240  ixpfi2  9303  elfi2  9370  fisn  9383  unxpwdom2  9546  cantnfp1lem3  9645  djulf1o  9894  djurf1o  9895  djur  9901  eldju2ndl  9906  eldju2ndr  9907  isfin4p1  10294  dcomex  10426  iundom2g  10519  fpwwe2lem12  10622  canthp1lem2  10633  0tsk  10735  elreal2  11112  ax1rid  11141  ltxrlt  11275  un0addcl  12532  un0mulcl  12533  fzodisjsn  13722  elfzonlteqm1  13766  elfzo0l  13781  elfzr  13806  elfzlmr  13807  seqf1o  14075  seqid3  14078  seqz  14082  1exp  14123  hashnn0pnf  14374  hash1elsn  14403  hashprg  14427  cats1un  14754  fsumss  15772  sumsnf  15790  fsumsplitsn  15791  fsum2dlem  15817  fsumcom2  15821  ackbijnn  15878  fprodss  15998  fprod2dlem  16030  fprodcom2  16034  fprodsplitsn  16039  sumeven  16440  sumodd  16441  divalgmod  16459  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  phi1  16827  dfphi2  16828  nnnn0modprm0  16861  ramubcl  17073  0ram  17075  ramz  17080  imasvscafn  17586  mreexmrid  17694  2initoinv  18062  2termoinv  18069  gsumress  18735  gsumval2  18739  smndex1basss  18962  smndex1mndlem  18966  0nsg  19230  symgextf1lem  19485  symgextf1  19486  pmtrprfval  19552  psgnsn  19585  lsmdisj2  19747  subgdisj1  19756  lt6abl  19960  gsumsnfd  20016  gsumzunsnd  20021  gsumunsnfd  20022  gsum2dlem2  20036  dprdfeq0  20089  dprdsn  20103  dprd2da  20109  pgpfac1lem3a  20143  pgpfaclem2  20149  ablsimpnosubgd  20171  c0snmgmhm  20540  0ring01eq  20627  zrinitorngc  20741  lsssn0  21069  lspsneq0  21133  lspdisjb  21250  pidlnz  21374  0ringprmidl  21477  pzriprnglem12  21642  frgpcyg  21723  obselocv  21878  obs2ss  21879  mplcoe5  22191  psdmul  22329  coe1tm  22434  mat0dim0  22624  mat0dimid  22625  mat0dimscm  22626  mat1dimscm  22632  mavmul0g  22710  mdet0pr  22749  mdetunilem9  22777  cramer0  22847  pmatcollpw3fi1lem1  22943  basdif0  23110  ordtbas  23349  ordtrest2  23361  cmpfi  23565  refun0  23672  txdis1cn  23792  ptrescn  23796  txkgen  23809  xkoptsub  23811  ordthmeolem  23958  pt1hmeo  23963  filconn  24040  filufint  24077  flimclslem  24141  ptcmplem3  24211  idnghm  24900  iccpnfcnv  25103  iccpnfhmeo  25104  bndth  25117  ivthicc  25617  ovoliunlem1  25661  i1fima2sn  25839  i1f1  25849  itg1addlem4  25858  itg1addlem5  25859  i1fmulc  25862  limcres  26045  limccnp  26050  limccnp2  26051  degltlem1  26229  ply1rem  26323  fta1blem  26328  ig1pdvds  26337  plyeq0lem  26367  plypf1  26369  plyaddlem1  26370  plymullem1  26371  coemulhi  26411  plycj  26434  plycjOLD  26436  plyn0mulidp  26442  taylfval  26522  abelthlem3  26596  rlimcnp  27130  wilthlem2  27233  logexprlim  27389  2sqreultblem  27612  tgldim0eq  28772  edglnl  29493  nbgr1vtx  29708  vtxdginducedm1lem4  29892  clwlkclwwlklem2a4  30348  eucrct2eupth  30596  frgrncvvdeqlem9  30658  nsnlplig  30833  nsnlpligALT  30834  fsumiunle  33173  cshw1s2  33280  gsumhashmul  33387  xrge0tsmsbi  33394  gsumwrd2dccatlem  33397  cyc3evpm  33470  0ringcring  33572  elrspunidl  33736  drngmxidlr  33760  ig1pmindeg  33892  0mplrim  33904  selvply1rhmlemb  33909  mplmulmvr  33929  vieta  33970  lbslsat  34006  lindsunlem  34014  irngnminplynz  34102  ordtrest2NEW  34313  xrge0iifcnv  34323  xrge0iifhom  34327  esumsnf  34454  esumpr  34456  esumiun  34484  inelpisys  34544  measvunilem0  34603  measvuni  34604  carsggect  34708  omsmeas  34713  repr0  34998  bnj98  35255  bnj1442  35437  bnj1452  35440  subfacp1lem5  35676  erdszelem4  35686  erdszelem8  35690  sconnpi1  35731  cvmlift2lem6  35800  cvmlift2lem12  35806  fmla0xp  35875  onint1  36960  dfttc4lem2  37040  bj-1nel0  37590  bj-sngltag  37619  bj-projval  37632  bj-elsn0  37799  bj-fununsn1  37897  tan2h  38263  lindsenlbs  38266  matunitlindf  38269  ptrest  38270  poimirlem23  38294  poimirlem24  38295  poimirlem25  38296  poimirlem28  38299  poimirlem29  38300  poimirlem30  38301  poimirlem31  38302  poimirlem32  38303  prdsbnd  38444  rrnequiv  38486  grpokerinj  38544  rngoueqz  38591  gidsn  38603  0rngo  38678  isdmn3  38725  dibelval2nd  41926  hdmaprnlem9N  42631  hdmap14lem4a  42645  dvrelog2b  42833  sticksstones11  42923  unitscyglem2  42963  0prjspnrel  43359  hbtlem5  43855  flcidc  43897  safesnsupfiss  44141  frege133d  44491  radcnvrat  45024  unisnALT  45634  sumsnd  45746  fnchoice  45749  rnsnf  45902  founiiun0  45908  elmapsnd  45921  fsneqrn  45927  infxrpnf  46160  supminfxr2  46183  cncfiooicc  46608  fperdvper  46633  dvmptfprodlem  46658  dvnprodlem1  46660  dvnprodlem2  46661  itgcoscmulx  46683  stoweidlem44  46758  fourierdlem49  46869  fourierdlem56  46876  fourierdlem80  46900  fourierdlem93  46913  fourierdlem101  46921  sge00  47090  sge0sn  47093  sge0snmpt  47097  sge0iunmptlemfi  47127  sge0p1  47128  sge0fodjrnlem  47130  sge0snmptf  47151  sge0splitsn  47155  nnfoctbdjlem  47169  meadjiunlem  47179  ismeannd  47181  caratheodorylem1  47240  isomenndlem  47244  hoidmv1le  47308  hoidmvlelem2  47310  hoidmvlelem3  47311  ovnhoilem1  47315  hoiqssbl  47339  ovnovollem1  47370  ovnovollem2  47371  chnerlem1  47598  eldmressn  47774  iccpartltu  48174  sbgoldbo  48552  nnsum3primesprm  48555  bgoldbtbndlem3  48572  stgr1  48726  gpgprismgr4cycllem7  48866  isidom3  49110  ldepspr  49253  lmod1zr  49273  termcbas2  50260  idfudiag1  50303