Theorem elsni 4602

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4586

This theorem is referenced by:  elsnd  4603  elsn2g  4624  nelsn  4626  elpwunsn  4644  eqoreldif  4645  disjsn2  4672  rabsnifsb  4682  sssn  4786  disjxsn  5096  opth1  5430  sosn  5718  ressn  6246  elsnxp  6252  elsuci  6389  funcnvsn  6550  funopdmsn  7104  fvconst  7118  fnsnr  7119  fmptap  7126  mposnif  7485  resf1extb  7890  1stconst  8056  2ndconst  8057  reldmtpos  8190  tpostpos  8202  disjen  9075  map2xp  9088  en1eqsn  9195  ac6sfi  9207  ixpfi2  9277  elfi2  9341  fisn  9354  unxpwdom2  9517  cantnfp1lem3  9609  djulf1o  9841  djurf1o  9842  djur  9848  eldju2ndl  9853  eldju2ndr  9854  isfin4p1  10244  dcomex  10376  iundom2g  10469  fpwwe2lem12  10571  canthp1lem2  10582  0tsk  10684  elreal2  11061  ax1rid  11090  ltxrlt  11220  un0addcl  12451  un0mulcl  12452  fzodisjsn  13634  elfzonlteqm1  13678  elfzo0l  13693  elfzr  13717  elfzlmr  13718  seqf1o  13984  seqid3  13987  seqz  13991  1exp  14032  hashnn0pnf  14283  hash1elsn  14312  hashprg  14336  cats1un  14662  fsumss  15667  sumsnf  15685  fsumsplitsn  15686  fsum2dlem  15712  fsumcom2  15716  ackbijnn  15770  fprodss  15890  fprod2dlem  15922  fprodcom2  15926  fprodsplitsn  15931  sumeven  16333  sumodd  16334  divalgmod  16352  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  phi1  16719  dfphi2  16720  nnnn0modprm0  16753  ramubcl  16965  0ram  16967  ramz  16972  imasvscafn  17476  mreexmrid  17584  2initoinv  17952  2termoinv  17959  gsumress  18591  gsumval2  18595  smndex1basss  18814  smndex1mndlem  18818  0nsg  19083  symgextf1lem  19334  symgextf1  19335  pmtrprfval  19401  psgnsn  19434  lsmdisj2  19596  subgdisj1  19605  lt6abl  19809  gsumsnfd  19865  gsumzunsnd  19870  gsumunsnfd  19871  gsum2dlem2  19885  dprdfeq0  19938  dprdsn  19952  dprd2da  19958  pgpfac1lem3a  19992  pgpfaclem2  19998  ablsimpnosubgd  20020  c0snmgmhm  20382  0ring01eq  20449  zrinitorngc  20562  lsssn0  20886  lspsneq0  20950  lspdisjb  21068  pzriprnglem12  21434  frgpcyg  21515  obselocv  21670  obs2ss  21671  mplcoe5  21980  psdmul  22086  coe1tm  22192  mat0dim0  22387  mat0dimid  22388  mat0dimscm  22389  mat1dimscm  22395  mavmul0g  22473  mdet0pr  22512  mdetunilem9  22540  cramer0  22610  pmatcollpw3fi1lem1  22706  basdif0  22873  ordtbas  23112  ordtrest2  23124  cmpfi  23328  refun0  23435  txdis1cn  23555  ptrescn  23559  txkgen  23572  xkoptsub  23574  ordthmeolem  23721  pt1hmeo  23726  filconn  23803  filufint  23840  flimclslem  23904  ptcmplem3  23974  idnghm  24664  iccpnfcnv  24875  iccpnfhmeo  24876  bndth  24890  ivthicc  25392  ovoliunlem1  25436  i1fima2sn  25614  i1f1  25624  itg1addlem4  25633  itg1addlem5  25634  i1fmulc  25637  limcres  25820  limccnp  25825  limccnp2  25826  degltlem1  26010  ply1rem  26104  fta1blem  26109  ig1pdvds  26118  plyeq0lem  26148  plypf1  26150  plyaddlem1  26151  plymullem1  26152  coemulhi  26192  plycj  26216  plycjOLD  26218  taylfval  26299  abelthlem3  26376  rlimcnp  26908  wilthlem2  27012  logexprlim  27169  2sqreultblem  27392  tgldim0eq  28483  edglnl  29123  nbgr1vtx  29338  vtxdginducedm1lem4  29523  clwlkclwwlklem2a4  29976  eucrct2eupth  30224  frgrncvvdeqlem9  30286  nsnlplig  30460  nsnlpligALT  30461  fsumiunle  32804  cshw1s2  32932  gsumhashmul  33044  xrge0tsmsbi  33046  gsumwrd2dccatlem  33049  cyc3evpm  33122  0ringcring  33219  pidlnz  33340  elrspunidl  33392  0ringprmidl  33413  drngmxidlr  33442  ig1pmindeg  33560  lbslsat  33605  lindsunlem  33613  irngnminplynz  33695  ordtrest2NEW  33906  xrge0iifcnv  33916  xrge0iifhom  33920  esumsnf  34047  esumpr  34049  esumiun  34077  inelpisys  34137  measvunilem0  34196  measvuni  34197  carsggect  34302  omsmeas  34307  plymulx0  34531  repr0  34595  bnj98  34850  bnj1442  35032  bnj1452  35035  subfacp1lem5  35164  erdszelem4  35174  erdszelem8  35178  sconnpi1  35219  cvmlift2lem6  35288  cvmlift2lem12  35294  fmla0xp  35363  onint1  36430  bj-1nel0  36935  bj-sngltag  36964  bj-projval  36977  bj-elsn0  37136  bj-fununsn1  37234  tan2h  37599  lindsenlbs  37602  matunitlindf  37605  ptrest  37606  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem28  37635  poimirlem29  37636  poimirlem30  37637  poimirlem31  37638  poimirlem32  37639  prdsbnd  37780  rrnequiv  37822  grpokerinj  37880  rngoueqz  37927  gidsn  37939  0rngo  38014  isdmn3  38061  dibelval2nd  41139  hdmaprnlem9N  41844  hdmap14lem4a  41858  dvrelog2b  42047  sticksstones11  42137  unitscyglem2  42177  0prjspnrel  42608  hbtlem5  43110  flcidc  43152  safesnsupfiss  43397  frege133d  43747  radcnvrat  44296  unisnALT  44908  sumsnd  45013  fnchoice  45016  rnsnf  45171  founiiun0  45177  elmapsnd  45191  fsneqrn  45198  infxrpnf  45435  supminfxr2  45458  cncfiooicc  45885  fperdvper  45910  dvmptfprodlem  45935  dvnprodlem1  45937  dvnprodlem2  45938  itgcoscmulx  45960  stoweidlem44  46035  fourierdlem49  46146  fourierdlem56  46153  fourierdlem80  46177  fourierdlem93  46190  fourierdlem101  46198  sge00  46367  sge0sn  46370  sge0snmpt  46374  sge0iunmptlemfi  46404  sge0p1  46405  sge0fodjrnlem  46407  sge0snmptf  46428  sge0splitsn  46432  nnfoctbdjlem  46446  meadjiunlem  46456  ismeannd  46458  caratheodorylem1  46517  isomenndlem  46521  hoidmv1le  46585  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnhoilem1  46592  hoiqssbl  46616  ovnovollem1  46647  ovnovollem2  46648  eldmressn  47031  iccpartltu  47419  sbgoldbo  47781  nnsum3primesprm  47784  bgoldbtbndlem3  47801  stgr1  47953  gpgprismgr4cycllem7  48084  ldepspr  48455  lmod1zr  48475  termcbas2  49464  idfudiag1  49507