Theorem elsni 4606

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

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

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 4590

This theorem is referenced by:  elsnd  4607  elsn2g  4628  nelsn  4630  elpwunsn  4648  eqoreldif  4649  disjsn2  4676  rabsnifsb  4686  sssn  4790  disjxsn  5101  opth1  5435  sosn  5725  ressn  6258  elsnxp  6264  elsuci  6401  funcnvsn  6566  funopdmsn  7122  fvconst  7136  fnsnr  7137  fmptap  7144  mposnif  7505  resf1extb  7910  1stconst  8079  2ndconst  8080  reldmtpos  8213  tpostpos  8225  disjen  9098  map2xp  9111  en1eqsn  9219  ac6sfi  9231  ixpfi2  9301  elfi2  9365  fisn  9378  unxpwdom2  9541  cantnfp1lem3  9633  djulf1o  9865  djurf1o  9866  djur  9872  eldju2ndl  9877  eldju2ndr  9878  isfin4p1  10268  dcomex  10400  iundom2g  10493  fpwwe2lem12  10595  canthp1lem2  10606  0tsk  10708  elreal2  11085  ax1rid  11114  ltxrlt  11244  un0addcl  12475  un0mulcl  12476  fzodisjsn  13658  elfzonlteqm1  13702  elfzo0l  13717  elfzr  13741  elfzlmr  13742  seqf1o  14008  seqid3  14011  seqz  14015  1exp  14056  hashnn0pnf  14307  hash1elsn  14336  hashprg  14360  cats1un  14686  fsumss  15691  sumsnf  15709  fsumsplitsn  15710  fsum2dlem  15736  fsumcom2  15740  ackbijnn  15794  fprodss  15914  fprod2dlem  15946  fprodcom2  15950  fprodsplitsn  15955  sumeven  16357  sumodd  16358  divalgmod  16376  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  phi1  16743  dfphi2  16744  nnnn0modprm0  16777  ramubcl  16989  0ram  16991  ramz  16996  imasvscafn  17500  mreexmrid  17604  2initoinv  17972  2termoinv  17979  gsumress  18609  gsumval2  18613  smndex1basss  18832  smndex1mndlem  18836  0nsg  19101  symgextf1lem  19350  symgextf1  19351  pmtrprfval  19417  psgnsn  19450  lsmdisj2  19612  subgdisj1  19621  lt6abl  19825  gsumsnfd  19881  gsumzunsnd  19886  gsumunsnfd  19887  gsum2dlem2  19901  dprdfeq0  19954  dprdsn  19968  dprd2da  19974  pgpfac1lem3a  20008  pgpfaclem2  20014  ablsimpnosubgd  20036  c0snmgmhm  20371  0ring01eq  20438  zrinitorngc  20551  lsssn0  20854  lspsneq0  20918  lspdisjb  21036  pzriprnglem12  21402  frgpcyg  21483  obselocv  21637  obs2ss  21638  mplcoe5  21947  psdmul  22053  coe1tm  22159  mat0dim0  22354  mat0dimid  22355  mat0dimscm  22356  mat1dimscm  22362  mavmul0g  22440  mdet0pr  22479  mdetunilem9  22507  cramer0  22577  pmatcollpw3fi1lem1  22673  basdif0  22840  ordtbas  23079  ordtrest2  23091  cmpfi  23295  refun0  23402  txdis1cn  23522  ptrescn  23526  txkgen  23539  xkoptsub  23541  ordthmeolem  23688  pt1hmeo  23693  filconn  23770  filufint  23807  flimclslem  23871  ptcmplem3  23941  idnghm  24631  iccpnfcnv  24842  iccpnfhmeo  24843  bndth  24857  ivthicc  25359  ovoliunlem1  25403  i1fima2sn  25581  i1f1  25591  itg1addlem4  25600  itg1addlem5  25601  i1fmulc  25604  limcres  25787  limccnp  25792  limccnp2  25793  degltlem1  25977  ply1rem  26071  fta1blem  26076  ig1pdvds  26085  plyeq0lem  26115  plypf1  26117  plyaddlem1  26118  plymullem1  26119  coemulhi  26159  plycj  26183  plycjOLD  26185  taylfval  26266  abelthlem3  26343  rlimcnp  26875  wilthlem2  26979  logexprlim  27136  2sqreultblem  27359  tgldim0eq  28430  edglnl  29070  nbgr1vtx  29285  vtxdginducedm1lem4  29470  clwlkclwwlklem2a4  29926  eucrct2eupth  30174  frgrncvvdeqlem9  30236  nsnlplig  30410  nsnlpligALT  30411  fsumiunle  32754  cshw1s2  32882  gsumhashmul  33001  xrge0tsmsbi  33003  gsumwrd2dccatlem  33006  cyc3evpm  33107  0ringcring  33203  pidlnz  33347  elrspunidl  33399  0ringprmidl  33420  drngmxidlr  33449  ig1pmindeg  33567  lbslsat  33612  lindsunlem  33620  irngnminplynz  33702  ordtrest2NEW  33913  xrge0iifcnv  33923  xrge0iifhom  33927  esumsnf  34054  esumpr  34056  esumiun  34084  inelpisys  34144  measvunilem0  34203  measvuni  34204  carsggect  34309  omsmeas  34314  plymulx0  34538  repr0  34602  bnj98  34857  bnj1442  35039  bnj1452  35042  subfacp1lem5  35171  erdszelem4  35181  erdszelem8  35185  sconnpi1  35226  cvmlift2lem6  35295  cvmlift2lem12  35301  fmla0xp  35370  onint1  36437  bj-1nel0  36942  bj-sngltag  36971  bj-projval  36984  bj-elsn0  37143  bj-fununsn1  37241  tan2h  37606  lindsenlbs  37609  matunitlindf  37612  ptrest  37613  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  prdsbnd  37787  rrnequiv  37829  grpokerinj  37887  rngoueqz  37934  gidsn  37946  0rngo  38021  isdmn3  38068  dibelval2nd  41146  hdmaprnlem9N  41851  hdmap14lem4a  41865  dvrelog2b  42054  sticksstones11  42144  unitscyglem2  42184  0prjspnrel  42615  hbtlem5  43117  flcidc  43159  safesnsupfiss  43404  frege133d  43754  radcnvrat  44303  unisnALT  44915  sumsnd  45020  fnchoice  45023  rnsnf  45178  founiiun0  45184  elmapsnd  45198  fsneqrn  45205  infxrpnf  45442  supminfxr2  45465  cncfiooicc  45892  fperdvper  45917  dvmptfprodlem  45942  dvnprodlem1  45944  dvnprodlem2  45945  itgcoscmulx  45967  stoweidlem44  46042  fourierdlem49  46153  fourierdlem56  46160  fourierdlem80  46184  fourierdlem93  46197  fourierdlem101  46205  sge00  46374  sge0sn  46377  sge0snmpt  46381  sge0iunmptlemfi  46411  sge0p1  46412  sge0fodjrnlem  46414  sge0snmptf  46435  sge0splitsn  46439  nnfoctbdjlem  46453  meadjiunlem  46463  ismeannd  46465  caratheodorylem1  46524  isomenndlem  46528  hoidmv1le  46592  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  hoiqssbl  46623  ovnovollem1  46654  ovnovollem2  46655  eldmressn  47038  iccpartltu  47426  sbgoldbo  47788  nnsum3primesprm  47791  bgoldbtbndlem3  47808  stgr1  47960  gpgprismgr4cycllem7  48091  ldepspr  48462  lmod1zr  48482  termcbas2  49471  idfudiag1  49514