Theorem elsni 4609

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sn 4593

This theorem is referenced by:  elsnd  4610  elsn2g  4631  nelsn  4633  elpwunsn  4651  eqoreldif  4652  disjsn2  4679  rabsnifsb  4689  sssn  4793  disjxsn  5104  opth1  5438  sosn  5728  ressn  6261  elsnxp  6267  elsuci  6404  funcnvsn  6569  funopdmsn  7125  fvconst  7139  fnsnr  7140  fmptap  7147  mposnif  7508  resf1extb  7913  1stconst  8082  2ndconst  8083  reldmtpos  8216  tpostpos  8228  disjen  9104  map2xp  9117  en1eqsn  9226  ac6sfi  9238  ixpfi2  9308  elfi2  9372  fisn  9385  unxpwdom2  9548  cantnfp1lem3  9640  djulf1o  9872  djurf1o  9873  djur  9879  eldju2ndl  9884  eldju2ndr  9885  isfin4p1  10275  dcomex  10407  iundom2g  10500  fpwwe2lem12  10602  canthp1lem2  10613  0tsk  10715  elreal2  11092  ax1rid  11121  ltxrlt  11251  un0addcl  12482  un0mulcl  12483  fzodisjsn  13665  elfzonlteqm1  13709  elfzo0l  13724  elfzr  13748  elfzlmr  13749  seqf1o  14015  seqid3  14018  seqz  14022  1exp  14063  hashnn0pnf  14314  hash1elsn  14343  hashprg  14367  cats1un  14693  fsumss  15698  sumsnf  15716  fsumsplitsn  15717  fsum2dlem  15743  fsumcom2  15747  ackbijnn  15801  fprodss  15921  fprod2dlem  15953  fprodcom2  15957  fprodsplitsn  15962  sumeven  16364  sumodd  16365  divalgmod  16383  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  phi1  16750  dfphi2  16751  nnnn0modprm0  16784  ramubcl  16996  0ram  16998  ramz  17003  imasvscafn  17507  mreexmrid  17611  2initoinv  17979  2termoinv  17986  gsumress  18616  gsumval2  18620  smndex1basss  18839  smndex1mndlem  18843  0nsg  19108  symgextf1lem  19357  symgextf1  19358  pmtrprfval  19424  psgnsn  19457  lsmdisj2  19619  subgdisj1  19628  lt6abl  19832  gsumsnfd  19888  gsumzunsnd  19893  gsumunsnfd  19894  gsum2dlem2  19908  dprdfeq0  19961  dprdsn  19975  dprd2da  19981  pgpfac1lem3a  20015  pgpfaclem2  20021  ablsimpnosubgd  20043  c0snmgmhm  20378  0ring01eq  20445  zrinitorngc  20558  lsssn0  20861  lspsneq0  20925  lspdisjb  21043  pzriprnglem12  21409  frgpcyg  21490  obselocv  21644  obs2ss  21645  mplcoe5  21954  psdmul  22060  coe1tm  22166  mat0dim0  22361  mat0dimid  22362  mat0dimscm  22363  mat1dimscm  22369  mavmul0g  22447  mdet0pr  22486  mdetunilem9  22514  cramer0  22584  pmatcollpw3fi1lem1  22680  basdif0  22847  ordtbas  23086  ordtrest2  23098  cmpfi  23302  refun0  23409  txdis1cn  23529  ptrescn  23533  txkgen  23546  xkoptsub  23548  ordthmeolem  23695  pt1hmeo  23700  filconn  23777  filufint  23814  flimclslem  23878  ptcmplem3  23948  idnghm  24638  iccpnfcnv  24849  iccpnfhmeo  24850  bndth  24864  ivthicc  25366  ovoliunlem1  25410  i1fima2sn  25588  i1f1  25598  itg1addlem4  25607  itg1addlem5  25608  i1fmulc  25611  limcres  25794  limccnp  25799  limccnp2  25800  degltlem1  25984  ply1rem  26078  fta1blem  26083  ig1pdvds  26092  plyeq0lem  26122  plypf1  26124  plyaddlem1  26125  plymullem1  26126  coemulhi  26166  plycj  26190  plycjOLD  26192  taylfval  26273  abelthlem3  26350  rlimcnp  26882  wilthlem2  26986  logexprlim  27143  2sqreultblem  27366  tgldim0eq  28437  edglnl  29077  nbgr1vtx  29292  vtxdginducedm1lem4  29477  clwlkclwwlklem2a4  29933  eucrct2eupth  30181  frgrncvvdeqlem9  30243  nsnlplig  30417  nsnlpligALT  30418  fsumiunle  32761  cshw1s2  32889  gsumhashmul  33008  xrge0tsmsbi  33010  gsumwrd2dccatlem  33013  cyc3evpm  33114  0ringcring  33210  pidlnz  33354  elrspunidl  33406  0ringprmidl  33427  drngmxidlr  33456  ig1pmindeg  33574  lbslsat  33619  lindsunlem  33627  irngnminplynz  33709  ordtrest2NEW  33920  xrge0iifcnv  33930  xrge0iifhom  33934  esumsnf  34061  esumpr  34063  esumiun  34091  inelpisys  34151  measvunilem0  34210  measvuni  34211  carsggect  34316  omsmeas  34321  plymulx0  34545  repr0  34609  bnj98  34864  bnj1442  35046  bnj1452  35049  subfacp1lem5  35178  erdszelem4  35188  erdszelem8  35192  sconnpi1  35233  cvmlift2lem6  35302  cvmlift2lem12  35308  fmla0xp  35377  onint1  36444  bj-1nel0  36949  bj-sngltag  36978  bj-projval  36991  bj-elsn0  37150  bj-fununsn1  37248  tan2h  37613  lindsenlbs  37616  matunitlindf  37619  ptrest  37620  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem28  37649  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  prdsbnd  37794  rrnequiv  37836  grpokerinj  37894  rngoueqz  37941  gidsn  37953  0rngo  38028  isdmn3  38075  dibelval2nd  41153  hdmaprnlem9N  41858  hdmap14lem4a  41872  dvrelog2b  42061  sticksstones11  42151  unitscyglem2  42191  0prjspnrel  42622  hbtlem5  43124  flcidc  43166  safesnsupfiss  43411  frege133d  43761  radcnvrat  44310  unisnALT  44922  sumsnd  45027  fnchoice  45030  rnsnf  45185  founiiun0  45191  elmapsnd  45205  fsneqrn  45212  infxrpnf  45449  supminfxr2  45472  cncfiooicc  45899  fperdvper  45924  dvmptfprodlem  45949  dvnprodlem1  45951  dvnprodlem2  45952  itgcoscmulx  45974  stoweidlem44  46049  fourierdlem49  46160  fourierdlem56  46167  fourierdlem80  46191  fourierdlem93  46204  fourierdlem101  46212  sge00  46381  sge0sn  46384  sge0snmpt  46388  sge0iunmptlemfi  46418  sge0p1  46419  sge0fodjrnlem  46421  sge0snmptf  46442  sge0splitsn  46446  nnfoctbdjlem  46460  meadjiunlem  46470  ismeannd  46472  caratheodorylem1  46531  isomenndlem  46535  hoidmv1le  46599  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem1  46606  hoiqssbl  46630  ovnovollem1  46661  ovnovollem2  46662  eldmressn  47042  iccpartltu  47430  sbgoldbo  47792  nnsum3primesprm  47795  bgoldbtbndlem3  47812  stgr1  47964  gpgprismgr4cycllem7  48095  ldepspr  48466  lmod1zr  48486  termcbas2  49475  idfudiag1  49518