Theorem elsni 4643

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sn 4627

This theorem is referenced by:  elsn2g  4664  nelsn  4666  elpwunsn  4684  eqoreldif  4685  disjsn2  4712  rabsnifsb  4722  sssn  4826  disjxsn  5137  opth1  5480  sosn  5772  ressn  6305  elsnxp  6311  elsuci  6451  funcnvsn  6616  funopdmsn  7170  fvconst  7184  fnsnr  7185  fmptap  7190  mposnif  7549  resf1extb  7956  1stconst  8125  2ndconst  8126  reldmtpos  8259  tpostpos  8271  disjen  9174  map2xp  9187  en1eqsn  9308  ac6sfi  9320  ixpfi2  9390  elfi2  9454  fisn  9467  unxpwdom2  9628  cantnfp1lem3  9720  djulf1o  9952  djurf1o  9953  djur  9959  eldju2ndl  9964  eldju2ndr  9965  isfin4p1  10355  dcomex  10487  iundom2g  10580  fpwwe2lem12  10682  canthp1lem2  10693  0tsk  10795  elreal2  11172  ax1rid  11201  ltxrlt  11331  un0addcl  12559  un0mulcl  12560  fzodisjsn  13737  elfzonlteqm1  13780  elfzo0l  13795  elfzr  13819  elfzlmr  13820  seqf1o  14084  seqid3  14087  seqz  14091  1exp  14132  hashnn0pnf  14381  hash1elsn  14410  hashprg  14434  cats1un  14759  fsumss  15761  sumsnf  15779  fsumsplitsn  15780  fsum2dlem  15806  fsumcom2  15810  ackbijnn  15864  fprodss  15984  fprod2dlem  16016  fprodcom2  16020  fprodsplitsn  16025  sumeven  16424  sumodd  16425  divalgmod  16443  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  phi1  16810  dfphi2  16811  nnnn0modprm0  16844  ramubcl  17056  0ram  17058  ramz  17063  imasvscafn  17582  mreexmrid  17686  2initoinv  18055  2termoinv  18062  gsumress  18695  gsumval2  18699  smndex1basss  18918  smndex1mndlem  18922  0nsg  19187  symgextf1lem  19438  symgextf1  19439  pmtrprfval  19505  psgnsn  19538  lsmdisj2  19700  subgdisj1  19709  lt6abl  19913  gsumsnfd  19969  gsumzunsnd  19974  gsumunsnfd  19975  gsum2dlem2  19989  dprdfeq0  20042  dprdsn  20056  dprd2da  20062  pgpfac1lem3a  20096  pgpfaclem2  20102  ablsimpnosubgd  20124  c0snmgmhm  20462  0ring01eq  20529  zrinitorngc  20642  lsssn0  20946  lspsneq0  21010  lspdisjb  21128  pzriprnglem12  21503  frgpcyg  21592  obselocv  21748  obs2ss  21749  mplcoe5  22058  psdmul  22170  coe1tm  22276  mat0dim0  22473  mat0dimid  22474  mat0dimscm  22475  mat1dimscm  22481  mavmul0g  22559  mdet0pr  22598  mdetunilem9  22626  cramer0  22696  pmatcollpw3fi1lem1  22792  basdif0  22960  ordtbas  23200  ordtrest2  23212  cmpfi  23416  refun0  23523  txdis1cn  23643  ptrescn  23647  txkgen  23660  xkoptsub  23662  ordthmeolem  23809  pt1hmeo  23814  filconn  23891  filufint  23928  flimclslem  23992  ptcmplem3  24062  idnghm  24764  iccpnfcnv  24975  iccpnfhmeo  24976  bndth  24990  ivthicc  25493  ovoliunlem1  25537  i1fima2sn  25715  i1f1  25725  itg1addlem4  25734  itg1addlem5  25735  i1fmulc  25738  limcres  25921  limccnp  25926  limccnp2  25927  degltlem1  26111  ply1rem  26205  fta1blem  26210  ig1pdvds  26219  plyeq0lem  26249  plypf1  26251  plyaddlem1  26252  plymullem1  26253  coemulhi  26293  plycj  26317  plycjOLD  26319  taylfval  26400  abelthlem3  26477  rlimcnp  27008  wilthlem2  27112  logexprlim  27269  2sqreultblem  27492  tgldim0eq  28511  edglnl  29160  nbgr1vtx  29375  vtxdginducedm1lem4  29560  clwlkclwwlklem2a4  30016  eucrct2eupth  30264  frgrncvvdeqlem9  30326  nsnlplig  30500  nsnlpligALT  30501  elsnd  32547  fsumiunle  32831  cshw1s2  32945  gsumhashmul  33064  xrge0tsmsbi  33066  gsumwrd2dccatlem  33069  cyc3evpm  33170  0ringcring  33256  pidlnz  33404  elrspunidl  33456  0ringprmidl  33477  drngmxidlr  33506  ig1pmindeg  33622  lbslsat  33667  lindsunlem  33675  irngnminplynz  33755  ordtrest2NEW  33922  xrge0iifcnv  33932  xrge0iifhom  33936  esumsnf  34065  esumpr  34067  esumiun  34095  inelpisys  34155  measvunilem0  34214  measvuni  34215  carsggect  34320  omsmeas  34325  plymulx0  34562  repr0  34626  bnj98  34881  bnj1442  35063  bnj1452  35066  subfacp1lem5  35189  erdszelem4  35199  erdszelem8  35203  sconnpi1  35244  cvmlift2lem6  35313  cvmlift2lem12  35319  fmla0xp  35388  onint1  36450  bj-1nel0  36955  bj-sngltag  36984  bj-projval  36997  bj-elsn0  37156  bj-fununsn1  37254  tan2h  37619  lindsenlbs  37622  matunitlindf  37625  ptrest  37626  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  prdsbnd  37800  rrnequiv  37842  grpokerinj  37900  rngoueqz  37947  gidsn  37959  0rngo  38034  isdmn3  38081  dibelval2nd  41154  hdmaprnlem9N  41859  hdmap14lem4a  41873  dvrelog2b  42067  sticksstones11  42157  unitscyglem2  42197  0prjspnrel  42637  hbtlem5  43140  flcidc  43182  safesnsupfiss  43428  frege133d  43778  radcnvrat  44333  unisnALT  44946  sumsnd  45031  fnchoice  45034  rnsnf  45189  founiiun0  45195  elmapsnd  45209  fsneqrn  45216  infxrpnf  45457  supminfxr2  45480  cncfiooicc  45909  fperdvper  45934  dvmptfprodlem  45959  dvnprodlem1  45961  dvnprodlem2  45962  itgcoscmulx  45984  stoweidlem44  46059  fourierdlem49  46170  fourierdlem56  46177  fourierdlem80  46201  fourierdlem93  46214  fourierdlem101  46222  sge00  46391  sge0sn  46394  sge0snmpt  46398  sge0iunmptlemfi  46428  sge0p1  46429  sge0fodjrnlem  46431  sge0snmptf  46452  sge0splitsn  46456  nnfoctbdjlem  46470  meadjiunlem  46480  ismeannd  46482  caratheodorylem1  46541  isomenndlem  46545  hoidmv1le  46609  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  hoiqssbl  46640  ovnovollem1  46671  ovnovollem2  46672  eldmressn  47049  iccpartltu  47412  sbgoldbo  47774  nnsum3primesprm  47777  bgoldbtbndlem3  47794  stgr1  47928  ldepspr  48390  lmod1zr  48410