Theorem elsni 4584

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4568

This theorem is referenced by:  elsnd  4585  elsn2g  4608  nelsn  4610  elpwunsn  4628  eqoreldif  4629  disjsn2  4656  rabsnifsb  4666  sssn  4769  disjxsn  5079  opth1  5428  sosn  5718  ressn  6249  elsnxp  6255  elsuci  6392  funcnvsn  6548  funopdmsn  7104  fvconst  7117  fnsnr  7118  fmptap  7125  mposnif  7483  resf1extb  7885  1stconst  8050  2ndconst  8051  reldmtpos  8184  tpostpos  8196  disjen  9072  map2xp  9085  en1eqsn  9185  ac6sfi  9194  ixpfi2  9260  elfi2  9327  fisn  9340  unxpwdom2  9503  cantnfp1lem3  9601  djulf1o  9836  djurf1o  9837  djur  9843  eldju2ndl  9848  eldju2ndr  9849  isfin4p1  10237  dcomex  10369  iundom2g  10462  fpwwe2lem12  10565  canthp1lem2  10576  0tsk  10678  elreal2  11055  ax1rid  11084  ltxrlt  11216  un0addcl  12470  un0mulcl  12471  fzodisjsn  13652  elfzonlteqm1  13696  elfzo0l  13711  elfzr  13736  elfzlmr  13737  seqf1o  14005  seqid3  14008  seqz  14012  1exp  14053  hashnn0pnf  14304  hash1elsn  14333  hashprg  14357  cats1un  14683  fsumss  15687  sumsnf  15705  fsumsplitsn  15706  fsum2dlem  15732  fsumcom2  15736  ackbijnn  15793  fprodss  15913  fprod2dlem  15945  fprodcom2  15949  fprodsplitsn  15954  sumeven  16356  sumodd  16357  divalgmod  16375  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  phi1  16743  dfphi2  16744  nnnn0modprm0  16777  ramubcl  16989  0ram  16991  ramz  16996  imasvscafn  17501  mreexmrid  17609  2initoinv  17977  2termoinv  17984  gsumress  18650  gsumval2  18654  smndex1basss  18876  smndex1mndlem  18880  0nsg  19144  symgextf1lem  19395  symgextf1  19396  pmtrprfval  19462  psgnsn  19495  lsmdisj2  19657  subgdisj1  19666  lt6abl  19870  gsumsnfd  19926  gsumzunsnd  19931  gsumunsnfd  19932  gsum2dlem2  19946  dprdfeq0  19999  dprdsn  20013  dprd2da  20019  pgpfac1lem3a  20053  pgpfaclem2  20059  ablsimpnosubgd  20081  c0snmgmhm  20442  0ring01eq  20506  zrinitorngc  20619  lsssn0  20943  lspsneq0  21007  lspdisjb  21124  pzriprnglem12  21472  frgpcyg  21553  obselocv  21708  obs2ss  21709  mplcoe5  22018  psdmul  22132  coe1tm  22238  mat0dim0  22432  mat0dimid  22433  mat0dimscm  22434  mat1dimscm  22440  mavmul0g  22518  mdet0pr  22557  mdetunilem9  22585  cramer0  22655  pmatcollpw3fi1lem1  22751  basdif0  22918  ordtbas  23157  ordtrest2  23169  cmpfi  23373  refun0  23480  txdis1cn  23600  ptrescn  23604  txkgen  23617  xkoptsub  23619  ordthmeolem  23766  pt1hmeo  23771  filconn  23848  filufint  23885  flimclslem  23949  ptcmplem3  24019  idnghm  24708  iccpnfcnv  24911  iccpnfhmeo  24912  bndth  24925  ivthicc  25425  ovoliunlem1  25469  i1fima2sn  25647  i1f1  25657  itg1addlem4  25666  itg1addlem5  25667  i1fmulc  25670  limcres  25853  limccnp  25858  limccnp2  25859  degltlem1  26037  ply1rem  26131  fta1blem  26136  ig1pdvds  26145  plyeq0lem  26175  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coemulhi  26219  plycj  26242  plycjOLD  26244  taylfval  26324  abelthlem3  26398  rlimcnp  26929  wilthlem2  27032  logexprlim  27188  2sqreultblem  27411  tgldim0eq  28571  edglnl  29212  nbgr1vtx  29427  vtxdginducedm1lem4  29611  clwlkclwwlklem2a4  30067  eucrct2eupth  30315  frgrncvvdeqlem9  30377  nsnlplig  30552  nsnlpligALT  30553  fsumiunle  32902  cshw1s2  33020  gsumhashmul  33128  xrge0tsmsbi  33135  gsumwrd2dccatlem  33138  cyc3evpm  33211  0ringcring  33313  pidlnz  33436  elrspunidl  33488  0ringprmidl  33509  drngmxidlr  33538  ig1pmindeg  33662  mplmulmvr  33683  vieta  33724  lbslsat  33760  lindsunlem  33768  irngnminplynz  33856  ordtrest2NEW  34067  xrge0iifcnv  34077  xrge0iifhom  34081  esumsnf  34208  esumpr  34210  esumiun  34238  inelpisys  34298  measvunilem0  34357  measvuni  34358  carsggect  34462  omsmeas  34467  plymulx0  34691  repr0  34755  bnj98  35009  bnj1442  35191  bnj1452  35194  subfacp1lem5  35366  erdszelem4  35376  erdszelem8  35380  sconnpi1  35421  cvmlift2lem6  35490  cvmlift2lem12  35496  fmla0xp  35565  onint1  36631  dfttc4lem2  36711  bj-1nel0  37261  bj-sngltag  37290  bj-projval  37303  bj-elsn0  37469  bj-fununsn1  37567  tan2h  37933  lindsenlbs  37936  matunitlindf  37939  ptrest  37940  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  prdsbnd  38114  rrnequiv  38156  grpokerinj  38214  rngoueqz  38261  gidsn  38273  0rngo  38348  isdmn3  38395  dibelval2nd  41598  hdmaprnlem9N  42303  hdmap14lem4a  42317  dvrelog2b  42505  sticksstones11  42595  unitscyglem2  42635  0prjspnrel  43060  hbtlem5  43556  flcidc  43598  safesnsupfiss  43842  frege133d  44192  radcnvrat  44741  unisnALT  45352  sumsnd  45457  fnchoice  45460  rnsnf  45614  founiiun0  45620  elmapsnd  45633  fsneqrn  45640  infxrpnf  45874  supminfxr2  45897  cncfiooicc  46322  fperdvper  46347  dvmptfprodlem  46372  dvnprodlem1  46374  dvnprodlem2  46375  itgcoscmulx  46397  stoweidlem44  46472  fourierdlem49  46583  fourierdlem56  46590  fourierdlem80  46614  fourierdlem93  46627  fourierdlem101  46635  sge00  46804  sge0sn  46807  sge0snmpt  46811  sge0iunmptlemfi  46841  sge0p1  46842  sge0fodjrnlem  46844  sge0snmptf  46865  sge0splitsn  46869  nnfoctbdjlem  46883  meadjiunlem  46893  ismeannd  46895  caratheodorylem1  46954  isomenndlem  46958  hoidmv1le  47022  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  hoiqssbl  47053  ovnovollem1  47084  ovnovollem2  47085  chnerlem1  47312  eldmressn  47485  iccpartltu  47885  sbgoldbo  48263  nnsum3primesprm  48266  bgoldbtbndlem3  48283  stgr1  48437  gpgprismgr4cycllem7  48577  ldepspr  48949  lmod1zr  48969  termcbas2  49957  idfudiag1  50000