Theorem elsni 4665

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sn 4649

This theorem is referenced by:  elsn2g  4686  nelsn  4688  elpwunsn  4707  eqoreldif  4708  disjsn2  4737  rabsnifsb  4747  sssn  4851  disjxsn  5160  opth1  5495  sosn  5786  ressn  6316  elsnxp  6322  elsuci  6462  funcnvsn  6628  funopdmsn  7184  fvconst  7198  fnsnr  7199  fmptap  7204  mposnif  7566  1stconst  8141  2ndconst  8142  reldmtpos  8275  tpostpos  8287  disjen  9200  map2xp  9213  en1eqsn  9336  ac6sfi  9348  ixpfi2  9420  elfi2  9483  fisn  9496  unxpwdom2  9657  cantnfp1lem3  9749  djulf1o  9981  djurf1o  9982  djur  9988  eldju2ndl  9993  eldju2ndr  9994  isfin4p1  10384  dcomex  10516  iundom2g  10609  fpwwe2lem12  10711  canthp1lem2  10722  0tsk  10824  elreal2  11201  ax1rid  11230  ltxrlt  11360  un0addcl  12586  un0mulcl  12587  fzodisjsn  13754  elfzonlteqm1  13792  elfzo0l  13806  elfzr  13830  elfzlmr  13831  seqf1o  14094  seqid3  14097  seqz  14101  1exp  14142  hashnn0pnf  14391  hash1elsn  14420  hashprg  14444  cats1un  14769  fsumss  15773  sumsnf  15791  fsumsplitsn  15792  fsum2dlem  15818  fsumcom2  15822  ackbijnn  15876  fprodss  15996  fprod2dlem  16028  fprodcom2  16032  fprodsplitsn  16037  sumeven  16435  sumodd  16436  divalgmod  16454  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  phi1  16820  dfphi2  16821  nnnn0modprm0  16853  ramubcl  17065  0ram  17067  ramz  17072  imasvscafn  17597  mreexmrid  17701  2initoinv  18077  2termoinv  18084  gsumress  18720  gsumval2  18724  smndex1basss  18940  smndex1mndlem  18944  0nsg  19209  symgextf1lem  19462  symgextf1  19463  pmtrprfval  19529  psgnsn  19562  lsmdisj2  19724  subgdisj1  19733  lt6abl  19937  gsumsnfd  19993  gsumzunsnd  19998  gsumunsnfd  19999  gsum2dlem2  20013  dprdfeq0  20066  dprdsn  20080  dprd2da  20086  pgpfac1lem3a  20120  pgpfaclem2  20126  ablsimpnosubgd  20148  c0snmgmhm  20488  0ring01eq  20555  zrinitorngc  20664  lsssn0  20969  lspsneq0  21033  lspdisjb  21151  pzriprnglem12  21526  frgpcyg  21615  obselocv  21771  obs2ss  21772  mplcoe5  22081  psdmul  22193  coe1tm  22297  mat0dim0  22494  mat0dimid  22495  mat0dimscm  22496  mat1dimscm  22502  mavmul0g  22580  mdet0pr  22619  mdetunilem9  22647  cramer0  22717  pmatcollpw3fi1lem1  22813  basdif0  22981  ordtbas  23221  ordtrest2  23233  cmpfi  23437  refun0  23544  txdis1cn  23664  ptrescn  23668  txkgen  23681  xkoptsub  23683  ordthmeolem  23830  pt1hmeo  23835  filconn  23912  filufint  23949  flimclslem  24013  ptcmplem3  24083  idnghm  24785  iccpnfcnv  24994  iccpnfhmeo  24995  bndth  25009  ivthicc  25512  ovoliunlem1  25556  i1fima2sn  25734  i1f1  25744  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  i1fmulc  25758  limcres  25941  limccnp  25946  limccnp2  25947  degltlem1  26131  ply1rem  26225  fta1blem  26230  ig1pdvds  26239  plyeq0lem  26269  plypf1  26271  plyaddlem1  26272  plymullem1  26273  coemulhi  26313  plycj  26337  taylfval  26418  abelthlem3  26495  rlimcnp  27026  wilthlem2  27130  logexprlim  27287  2sqreultblem  27510  tgldim0eq  28529  edglnl  29178  nbgr1vtx  29393  vtxdginducedm1lem4  29578  clwlkclwwlklem2a4  30029  eucrct2eupth  30277  frgrncvvdeqlem9  30339  nsnlplig  30513  nsnlpligALT  30514  fsumiunle  32833  cshw1s2  32927  gsumhashmul  33040  xrge0tsmsbi  33042  cyc3evpm  33143  0ringcring  33224  pidlnz  33369  elrspunidl  33421  0ringprmidl  33442  drngmxidlr  33471  ig1pmindeg  33587  lbslsat  33629  lindsunlem  33637  irngnminplynz  33705  ordtrest2NEW  33869  xrge0iifcnv  33879  xrge0iifhom  33883  esumsnf  34028  esumpr  34030  esumiun  34058  inelpisys  34118  measvunilem0  34177  measvuni  34178  carsggect  34283  omsmeas  34288  plymulx0  34524  repr0  34588  bnj98  34843  bnj1442  35025  bnj1452  35028  subfacp1lem5  35152  erdszelem4  35162  erdszelem8  35166  sconnpi1  35207  cvmlift2lem6  35276  cvmlift2lem12  35282  fmla0xp  35351  onint1  36415  bj-1nel0  36920  bj-sngltag  36949  bj-projval  36962  bj-elsn0  37121  bj-fununsn1  37219  tan2h  37572  lindsenlbs  37575  matunitlindf  37578  ptrest  37579  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem28  37608  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  prdsbnd  37753  rrnequiv  37795  grpokerinj  37853  rngoueqz  37900  gidsn  37912  0rngo  37987  isdmn3  38034  dibelval2nd  41109  hdmaprnlem9N  41814  hdmap14lem4a  41828  dvrelog2b  42023  sticksstones11  42113  unitscyglem2  42153  0prjspnrel  42582  hbtlem5  43085  flcidc  43131  safesnsupfiss  43377  frege133d  43727  radcnvrat  44283  unisnALT  44897  sumsnd  44926  fnchoice  44929  rnsnf  45091  founiiun0  45097  elmapsnd  45111  fsneqrn  45118  infxrpnf  45361  supminfxr2  45384  cncfiooicc  45815  fperdvper  45840  dvmptfprodlem  45865  dvnprodlem1  45867  dvnprodlem2  45868  itgcoscmulx  45890  stoweidlem44  45965  fourierdlem49  46076  fourierdlem56  46083  fourierdlem80  46107  fourierdlem93  46120  fourierdlem101  46128  sge00  46297  sge0sn  46300  sge0snmpt  46304  sge0iunmptlemfi  46334  sge0p1  46335  sge0fodjrnlem  46337  sge0snmptf  46358  sge0splitsn  46362  nnfoctbdjlem  46376  meadjiunlem  46386  ismeannd  46388  caratheodorylem1  46447  isomenndlem  46451  hoidmv1le  46515  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem1  46522  hoiqssbl  46546  ovnovollem1  46577  ovnovollem2  46578  eldmressn  46952  iccpartltu  47299  sbgoldbo  47661  nnsum3primesprm  47664  bgoldbtbndlem3  47681  ldepspr  48202  lmod1zr  48222