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  17580  2initoinv  17948  2termoinv  17955  gsumress  18585  gsumval2  18589  smndex1basss  18808  smndex1mndlem  18812  0nsg  19077  symgextf1lem  19326  symgextf1  19327  pmtrprfval  19393  psgnsn  19426  lsmdisj2  19588  subgdisj1  19597  lt6abl  19801  gsumsnfd  19857  gsumzunsnd  19862  gsumunsnfd  19863  gsum2dlem2  19877  dprdfeq0  19930  dprdsn  19944  dprd2da  19950  pgpfac1lem3a  19984  pgpfaclem2  19990  ablsimpnosubgd  20012  c0snmgmhm  20347  0ring01eq  20414  zrinitorngc  20527  lsssn0  20830  lspsneq0  20894  lspdisjb  21012  pzriprnglem12  21378  frgpcyg  21459  obselocv  21613  obs2ss  21614  mplcoe5  21923  psdmul  22029  coe1tm  22135  mat0dim0  22330  mat0dimid  22331  mat0dimscm  22332  mat1dimscm  22338  mavmul0g  22416  mdet0pr  22455  mdetunilem9  22483  cramer0  22553  pmatcollpw3fi1lem1  22649  basdif0  22816  ordtbas  23055  ordtrest2  23067  cmpfi  23271  refun0  23378  txdis1cn  23498  ptrescn  23502  txkgen  23515  xkoptsub  23517  ordthmeolem  23664  pt1hmeo  23669  filconn  23746  filufint  23783  flimclslem  23847  ptcmplem3  23917  idnghm  24607  iccpnfcnv  24818  iccpnfhmeo  24819  bndth  24833  ivthicc  25335  ovoliunlem1  25379  i1fima2sn  25557  i1f1  25567  itg1addlem4  25576  itg1addlem5  25577  i1fmulc  25580  limcres  25763  limccnp  25768  limccnp2  25769  degltlem1  25953  ply1rem  26047  fta1blem  26052  ig1pdvds  26061  plyeq0lem  26091  plypf1  26093  plyaddlem1  26094  plymullem1  26095  coemulhi  26135  plycj  26159  plycjOLD  26161  taylfval  26242  abelthlem3  26319  rlimcnp  26851  wilthlem2  26955  logexprlim  27112  2sqreultblem  27335  tgldim0eq  28406  edglnl  29046  nbgr1vtx  29261  vtxdginducedm1lem4  29446  clwlkclwwlklem2a4  29899  eucrct2eupth  30147  frgrncvvdeqlem9  30209  nsnlplig  30383  nsnlpligALT  30384  fsumiunle  32727  cshw1s2  32855  gsumhashmul  32974  xrge0tsmsbi  32976  gsumwrd2dccatlem  32979  cyc3evpm  33080  0ringcring  33176  pidlnz  33320  elrspunidl  33372  0ringprmidl  33393  drngmxidlr  33422  ig1pmindeg  33540  lbslsat  33585  lindsunlem  33593  irngnminplynz  33675  ordtrest2NEW  33886  xrge0iifcnv  33896  xrge0iifhom  33900  esumsnf  34027  esumpr  34029  esumiun  34057  inelpisys  34117  measvunilem0  34176  measvuni  34177  carsggect  34282  omsmeas  34287  plymulx0  34511  repr0  34575  bnj98  34830  bnj1442  35012  bnj1452  35015  subfacp1lem5  35144  erdszelem4  35154  erdszelem8  35158  sconnpi1  35199  cvmlift2lem6  35268  cvmlift2lem12  35274  fmla0xp  35343  onint1  36410  bj-1nel0  36915  bj-sngltag  36944  bj-projval  36957  bj-elsn0  37116  bj-fununsn1  37214  tan2h  37579  lindsenlbs  37582  matunitlindf  37585  ptrest  37586  poimirlem23  37610  poimirlem24  37611  poimirlem25  37612  poimirlem28  37615  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  prdsbnd  37760  rrnequiv  37802  grpokerinj  37860  rngoueqz  37907  gidsn  37919  0rngo  37994  isdmn3  38041  dibelval2nd  41119  hdmaprnlem9N  41824  hdmap14lem4a  41838  dvrelog2b  42027  sticksstones11  42117  unitscyglem2  42157  0prjspnrel  42588  hbtlem5  43090  flcidc  43132  safesnsupfiss  43377  frege133d  43727  radcnvrat  44276  unisnALT  44888  sumsnd  44993  fnchoice  44996  rnsnf  45151  founiiun0  45157  elmapsnd  45171  fsneqrn  45178  infxrpnf  45415  supminfxr2  45438  cncfiooicc  45865  fperdvper  45890  dvmptfprodlem  45915  dvnprodlem1  45917  dvnprodlem2  45918  itgcoscmulx  45940  stoweidlem44  46015  fourierdlem49  46126  fourierdlem56  46133  fourierdlem80  46157  fourierdlem93  46170  fourierdlem101  46178  sge00  46347  sge0sn  46350  sge0snmpt  46354  sge0iunmptlemfi  46384  sge0p1  46385  sge0fodjrnlem  46387  sge0snmptf  46408  sge0splitsn  46412  nnfoctbdjlem  46426  meadjiunlem  46436  ismeannd  46438  caratheodorylem1  46497  isomenndlem  46501  hoidmv1le  46565  hoidmvlelem2  46567  hoidmvlelem3  46568  ovnhoilem1  46572  hoiqssbl  46596  ovnovollem1  46627  ovnovollem2  46628  eldmressn  47011  iccpartltu  47399  sbgoldbo  47761  nnsum3primesprm  47764  bgoldbtbndlem3  47781  stgr1  47933  gpgprismgr4cycllem7  48064  ldepspr  48435  lmod1zr  48455  termcbas2  49444  idfudiag1  49487