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 266	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-sn 4568

This theorem is referenced by:  elsn2g  4605  nelsn  4607  elpwunsn  4625  eqoreldif  4626  disjsn2  4654  rabsnifsb  4664  sssn  4765  disjxsn  5072  opth1  5394  sosn  5674  ressn  6187  elsnxp  6193  elsuci  6331  funcnvsn  6482  funopdmsn  7019  fvconst  7033  fnsnr  7034  fmptap  7039  mposnif  7384  1stconst  7931  2ndconst  7932  reldmtpos  8041  tpostpos  8053  disjen  8903  map2xp  8916  ac6sfi  9036  ixpfi2  9095  elfi2  9151  fisn  9164  unxpwdom2  9325  cantnfp1lem3  9416  djulf1o  9671  djurf1o  9672  djur  9678  eldju2ndl  9683  eldju2ndr  9684  isfin4p1  10072  dcomex  10204  iundom2g  10297  fpwwe2lem12  10399  canthp1lem2  10410  0tsk  10512  elreal2  10889  ax1rid  10918  ltxrlt  11046  un0addcl  12266  un0mulcl  12267  fzodisjsn  13423  elfzonlteqm1  13461  elfzo0l  13475  elfzr  13498  elfzlmr  13499  seqf1o  13762  seqid3  13765  seqz  13769  1exp  13810  hashnn0pnf  14054  hash1elsn  14084  hashprg  14108  cats1un  14432  fsumss  15435  sumsnf  15453  fsumsplitsn  15454  fsum2dlem  15480  fsumcom2  15484  ackbijnn  15538  fprodss  15656  fprod2dlem  15688  fprodcom2  15692  fprodsplitsn  15697  sumeven  16094  sumodd  16095  divalgmod  16113  lcmfunsnlem2lem1  16341  lcmfunsnlem2lem2  16342  phi1  16472  dfphi2  16473  nnnn0modprm0  16505  ramubcl  16717  0ram  16719  ramz  16724  imasvscafn  17246  mreexmrid  17350  2initoinv  17723  2termoinv  17730  gsumress  18364  gsumval2  18368  smndex1basss  18542  smndex1mndlem  18546  0nsg  18795  symgextf1lem  19026  symgextf1  19027  pmtrprfval  19093  psgnsn  19126  lsmdisj2  19286  subgdisj1  19295  lt6abl  19494  gsumsnfd  19550  gsumzunsnd  19555  gsumunsnfd  19556  gsum2dlem2  19570  dprdfeq0  19623  dprdsn  19637  dprd2da  19643  pgpfac1lem3a  19677  pgpfaclem2  19683  ablsimpnosubgd  19705  lsssn0  20207  lspsneq0  20272  lspdisjb  20386  0ring01eq  20540  frgpcyg  20779  obselocv  20933  obs2ss  20934  mplcoe5  21239  coe1tm  21442  mat0dim0  21614  mat0dimid  21615  mat0dimscm  21616  mat1dimscm  21622  mavmul0g  21700  mdet0pr  21739  mdetunilem9  21767  cramer0  21837  pmatcollpw3fi1lem1  21933  basdif0  22101  ordtbas  22341  ordtrest2  22353  cmpfi  22557  refun0  22664  txdis1cn  22784  ptrescn  22788  txkgen  22801  xkoptsub  22803  ordthmeolem  22950  pt1hmeo  22955  filconn  23032  filufint  23069  flimclslem  23133  ptcmplem3  23203  idnghm  23905  iccpnfcnv  24105  iccpnfhmeo  24106  bndth  24119  ivthicc  24620  ovoliunlem1  24664  i1fima2sn  24842  i1f1  24852  itg1addlem4  24861  itg1addlem4OLD  24862  itg1addlem5  24863  i1fmulc  24866  limcres  25048  limccnp  25053  limccnp2  25054  degltlem1  25235  ply1rem  25326  fta1blem  25331  ig1pdvds  25339  plyeq0lem  25369  plypf1  25371  plyaddlem1  25372  plymullem1  25373  coemulhi  25413  plycj  25436  taylfval  25516  abelthlem3  25590  rlimcnp  26113  wilthlem2  26216  logexprlim  26371  2sqreultblem  26594  tgldim0eq  26862  edglnl  27511  nbgr1vtx  27723  vtxdginducedm1lem4  27907  clwlkclwwlklem2a4  28357  eucrct2eupth  28605  frgrncvvdeqlem9  28667  nsnlplig  28839  nsnlpligALT  28840  fsumiunle  31139  cshw1s2  31228  gsumhashmul  31312  xrge0tsmsbi  31314  cyc3evpm  31413  pidlnz  31567  elrspunidl  31602  0ringprmidl  31621  lbslsat  31695  lindsunlem  31701  ordtrest2NEW  31869  xrge0iifcnv  31879  xrge0iifhom  31883  esumsnf  32028  esumpr  32030  esumiun  32058  inelpisys  32118  measvunilem0  32177  measvuni  32178  carsggect  32281  omsmeas  32286  plymulx0  32522  repr0  32587  bnj98  32843  bnj1442  33025  bnj1452  33028  subfacp1lem5  33142  erdszelem4  33152  erdszelem8  33156  sconnpi1  33197  cvmlift2lem6  33266  cvmlift2lem12  33272  fmla0xp  33341  onint1  34634  bj-1nel0  35140  bj-sngltag  35169  bj-projval  35182  bj-elsn0  35322  bj-fununsn1  35420  tan2h  35765  lindsenlbs  35768  matunitlindf  35771  ptrest  35772  poimirlem23  35796  poimirlem24  35797  poimirlem25  35798  poimirlem28  35801  poimirlem29  35802  poimirlem30  35803  poimirlem31  35804  poimirlem32  35805  prdsbnd  35947  rrnequiv  35989  grpokerinj  36047  rngoueqz  36094  gidsn  36106  0rngo  36181  isdmn3  36228  dibelval2nd  39162  hdmaprnlem9N  39867  hdmap14lem4a  39881  dvrelog2b  40071  sticksstones11  40109  0prjspnrel  40461  hbtlem5  40950  flcidc  40996  frege133d  41343  radcnvrat  41902  unisnALT  42516  sumsnd  42539  fnchoice  42542  rnsnf  42691  founiiun0  42698  elmapsnd  42714  fsneqrn  42721  infxrpnf  42957  supminfxr2  42980  cncfiooicc  43406  fperdvper  43431  dvmptfprodlem  43456  dvnprodlem1  43458  dvnprodlem2  43459  itgcoscmulx  43481  stoweidlem44  43556  fourierdlem49  43667  fourierdlem56  43674  fourierdlem80  43698  fourierdlem93  43711  fourierdlem101  43719  sge00  43885  sge0sn  43888  sge0snmpt  43892  sge0iunmptlemfi  43922  sge0p1  43923  sge0fodjrnlem  43925  sge0snmptf  43946  sge0splitsn  43950  nnfoctbdjlem  43964  meadjiunlem  43974  ismeannd  43976  caratheodorylem1  44035  isomenndlem  44039  hoidmv1le  44103  hoidmvlelem2  44105  hoidmvlelem3  44106  ovnhoilem1  44110  hoiqssbl  44134  ovnovollem1  44165  ovnovollem2  44166  eldmressn  44499  iccpartltu  44846  sbgoldbo  45208  nnsum3primesprm  45211  bgoldbtbndlem3  45228  c0snmgmhm  45441  zrinitorngc  45527  ldepspr  45783  lmod1zr  45803