Theorem elsni 4601

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sn 4585

This theorem is used by:  elsnd  4602  elsn2g  4625  nelsn  4627  elpwunsn  4645  eqoreldif  4646  disjsn2  4673  rabsnifsb  4683  sssn  4787  disjxsn  5097  opth1  5444  sosn  5738  ressn  6288  elsnxp  6294  elsuci  6432  funcnvsn  6590  funopdmsn  7154  fvconst  7167  fnsnr  7168  fmptap  7175  mposnif  7536  resf1extb  7946  1stconst  8111  2ndconst  8112  reldmtpos  8251  tpostpos  8263  disjen  9153  map2xp  9166  en1eqsn  9266  ac6sfi  9275  ixpfi2  9339  elfi2  9406  fisn  9419  unxpwdom2  9582  cantnfp1lem3  9681  djulf1o  9993  djurf1o  9994  djur  10000  eldju2ndl  10005  eldju2ndr  10006  isfin4p1  10393  dcomex  10525  iundom2g  10624  fpwwe2lem12  10727  canthp1lem2  10738  0tsk  10840  elreal2  11217  ax1rid  11246  ltxrlt  11380  un0addcl  12639  un0mulcl  12640  fzodisjsn  13832  elfzonlteqm1  13876  elfzo0l  13891  elfzr  13916  elfzlmr  13917  seqf1o  14186  seqid3  14189  seqz  14193  1exp  14234  hashnn0pnf  14486  hash1elsn  14515  hashprg  14539  cats1un  14870  fsumss  15891  sumsnf  15909  fsumsplitsn  15910  fsum2dlem  15936  fsumcom2  15940  ackbijnn  15997  fprodss  16115  fprod2dlem  16147  fprodcom2  16151  fprodsplitsn  16156  sumeven  16557  sumodd  16558  divalgmod  16576  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  phi1  16950  dfphi2  16951  nnnn0modprm0  16984  ramubcl  17196  0ram  17198  ramz  17203  imasvscafn  17709  mreexmrid  17817  2initoinv  18185  2termoinv  18192  gsumress  18871  gsumval2  18875  smndex1basss  19104  smndex1mndlem  19108  0nsg  19379  symgextf1lem  19634  symgextf1  19635  pmtrprfval  19701  psgnsn  19734  lsmdisj2  19896  subgdisj1  19905  lt6abl  20109  gsumsnfd  20165  gsumzunsnd  20170  gsumunsnfd  20171  gsum2dlem2  20185  dprdfeq0  20238  dprdsn  20252  dprd2da  20258  pgpfac1lem3a  20292  pgpfaclem2  20298  ablsimpnosubgd  20320  c0snmgmhm  20692  0ring01eq  20780  zrinitorngc  20894  lsssn0  21223  lspsneq0  21287  lspdisjb  21404  pidlnz  21528  0ringprmidl  21633  pzriprnglem12  21798  frgpcyg  21879  obselocv  22034  obs2ss  22035  lindsenlbs  22157  mplcoe5  22349  psdmul  22487  coe1tm  22592  mat0dim0  22782  mat0dimid  22783  mat0dimscm  22784  mat1dimscm  22790  mavmul0g  22868  mdet0pr  22907  mdetunilem9  22935  matunitlindf  22996  cramer0  23008  pmatcollpw3fi1lem1  23104  basdif0  23271  ordtbas  23510  ordtrest2  23522  cmpfi  23726  refun0  23834  txdis1cn  23954  ptrescn  23958  txkgen  23971  xkoptsub  23973  ordthmeolem  24120  pt1hmeo  24125  filconn  24202  filufint  24239  flimclslem  24303  ptcmplem3  24373  idnghm  25062  iccpnfcnv  25265  iccpnfhmeo  25266  bndth  25279  ivthicc  25779  ovoliunlem1  25823  i1fima2sn  26001  i1f1  26011  itg1addlem4  26020  itg1addlem5  26021  i1fmulc  26024  limcres  26206  limccnp  26211  limccnp2  26212  degltlem1  26390  ply1rem  26484  fta1blem  26489  ig1pdvds  26498  plyeq0lem  26529  plypf1  26531  plyaddlem1  26532  plymullem1  26533  coemulhi  26573  plycj  26596  plyn0mulidp  26602  taylfval  26686  abelthlem3  26760  rlimcnp  27293  wilthlem2  27396  logexprlim  27552  2sqreultblem  27775  tgldim0eq  28966  edglnl  29721  nbgr1vtx  29939  vtxdginducedm1lem4  30123  clwlkclwwlklem2a4  30588  eucrct2eupth  30846  frgrncvvdeqlem9  30908  nsnlplig  31083  nsnlpligALT  31084  fsumiunle  33420  cshw1s2  33521  gsumhashmul  33628  xrge0tsmsbi  33635  gsumwrd2dccatlem  33638  cyc3evpm  33711  0ringcring  33813  elrspunidl  33978  drngmxidlr  34002  ig1pmindeg  34134  0mplrim  34146  selvply1rhmlemb  34151  mplmulmvr  34171  vieta  34212  lbslsat  34248  lindsunlem  34256  irngnminplynz  34344  ordtrest2NEW  34555  xrge0iifcnv  34565  xrge0iifhom  34569  esumsnf  34696  esumpr  34698  esumiun  34726  inelpisys  34787  measvunilem0  34846  measvuni  34847  carsggect  34950  omsmeas  34955  repr0  35240  bnj98  35497  bnj1442  35679  bnj1452  35682  subfacp1lem5  35949  erdszelem4  35959  erdszelem8  35963  sconnpi1  36004  cvmlift2lem6  36073  cvmlift2lem12  36079  fmla0xp  36148  onint1  37237  dfttc4lem2  37317  bj-1nel0  37867  bj-sngltag  37896  bj-projval  37909  bj-elsn0  38076  bj-fununsn1  38174  tan2h  38535  ptrest  38537  poimirlem23  38561  poimirlem24  38562  poimirlem25  38563  poimirlem28  38566  poimirlem29  38567  poimirlem30  38568  poimirlem31  38569  poimirlem32  38570  prdsbnd  38727  rrnequiv  38769  grpokerinj  38827  rngoueqz  38874  gidsn  38886  0rngo  38961  isdmn3  39008  dibelval2nd  42209  hdmaprnlem9N  42914  hdmap14lem4a  42928  dvrelog2b  43116  sticksstones11  43206  unitscyglem2  43246  0prjspnrel  43663  hbtlem5  44129  flcidc  44171  safesnsupfiss  44415  frege133d  44764  radcnvrat  45297  unisnALT  45907  sumsnd  46042  fnchoice  46045  rnsnf  46198  founiiun0  46204  elmapsnd  46217  fsneqrn  46223  infxrpnf  46455  supminfxr2  46478  cncfiooicc  46903  fperdvper  46928  dvmptfprodlem  46953  dvnprodlem1  46955  dvnprodlem2  46956  itgcoscmulx  46978  stoweidlem44  47053  fourierdlem49  47164  fourierdlem56  47171  fourierdlem80  47195  fourierdlem93  47208  fourierdlem101  47216  sge00  47385  sge0sn  47388  sge0snmpt  47392  sge0iunmptlemfi  47422  sge0p1  47423  sge0fodjrnlem  47425  sge0snmptf  47446  sge0splitsn  47450  nnfoctbdjlem  47464  meadjiunlem  47474  ismeannd  47476  caratheodorylem1  47535  isomenndlem  47539  hoidmv1le  47603  hoidmvlelem2  47605  hoidmvlelem3  47606  ovnhoilem1  47610  hoiqssbl  47634  ovnovollem1  47665  ovnovollem2  47666  eldmressn  48106  iccpartltu  48506  sbgoldbo  48884  nnsum3primesprm  48887  bgoldbtbndlem3  48904  stgr1  49058  gpgprismgr4cycllem7  49198  isidom3  49441  ldepspr  49584  lmod1zr  49604  termcbas2  50589  idfudiag1  50632