Theorem elsni 4595

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {csn 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-sn 4579

This theorem is referenced by:  elsnd  4596  elsn2g  4619  nelsn  4621  elpwunsn  4639  eqoreldif  4640  disjsn2  4667  rabsnifsb  4677  sssn  4780  disjxsn  5090  opth1  5421  sosn  5709  ressn  6241  elsnxp  6247  elsuci  6384  funcnvsn  6540  funopdmsn  7093  fvconst  7106  fnsnr  7107  fmptap  7114  mposnif  7472  resf1extb  7874  1stconst  8040  2ndconst  8041  reldmtpos  8174  tpostpos  8186  disjen  9060  map2xp  9073  en1eqsn  9173  ac6sfi  9182  ixpfi2  9248  elfi2  9315  fisn  9328  unxpwdom2  9491  cantnfp1lem3  9587  djulf1o  9822  djurf1o  9823  djur  9829  eldju2ndl  9834  eldju2ndr  9835  isfin4p1  10223  dcomex  10355  iundom2g  10448  fpwwe2lem12  10551  canthp1lem2  10562  0tsk  10664  elreal2  11041  ax1rid  11070  ltxrlt  11201  un0addcl  12432  un0mulcl  12433  fzodisjsn  13611  elfzonlteqm1  13655  elfzo0l  13670  elfzr  13695  elfzlmr  13696  seqf1o  13964  seqid3  13967  seqz  13971  1exp  14012  hashnn0pnf  14263  hash1elsn  14292  hashprg  14316  cats1un  14642  fsumss  15646  sumsnf  15664  fsumsplitsn  15665  fsum2dlem  15691  fsumcom2  15695  ackbijnn  15749  fprodss  15869  fprod2dlem  15901  fprodcom2  15905  fprodsplitsn  15910  sumeven  16312  sumodd  16313  divalgmod  16331  lcmfunsnlem2lem1  16563  lcmfunsnlem2lem2  16564  phi1  16698  dfphi2  16699  nnnn0modprm0  16732  ramubcl  16944  0ram  16946  ramz  16951  imasvscafn  17456  mreexmrid  17564  2initoinv  17932  2termoinv  17939  gsumress  18605  gsumval2  18609  smndex1basss  18828  smndex1mndlem  18832  0nsg  19096  symgextf1lem  19347  symgextf1  19348  pmtrprfval  19414  psgnsn  19447  lsmdisj2  19609  subgdisj1  19618  lt6abl  19822  gsumsnfd  19878  gsumzunsnd  19883  gsumunsnfd  19884  gsum2dlem2  19898  dprdfeq0  19951  dprdsn  19965  dprd2da  19971  pgpfac1lem3a  20005  pgpfaclem2  20011  ablsimpnosubgd  20033  c0snmgmhm  20396  0ring01eq  20460  zrinitorngc  20573  lsssn0  20897  lspsneq0  20961  lspdisjb  21079  pzriprnglem12  21445  frgpcyg  21526  obselocv  21681  obs2ss  21682  mplcoe5  21993  psdmul  22107  coe1tm  22213  mat0dim0  22409  mat0dimid  22410  mat0dimscm  22411  mat1dimscm  22417  mavmul0g  22495  mdet0pr  22534  mdetunilem9  22562  cramer0  22632  pmatcollpw3fi1lem1  22728  basdif0  22895  ordtbas  23134  ordtrest2  23146  cmpfi  23350  refun0  23457  txdis1cn  23577  ptrescn  23581  txkgen  23594  xkoptsub  23596  ordthmeolem  23743  pt1hmeo  23748  filconn  23825  filufint  23862  flimclslem  23926  ptcmplem3  23996  idnghm  24685  iccpnfcnv  24896  iccpnfhmeo  24897  bndth  24911  ivthicc  25413  ovoliunlem1  25457  i1fima2sn  25635  i1f1  25645  itg1addlem4  25654  itg1addlem5  25655  i1fmulc  25658  limcres  25841  limccnp  25846  limccnp2  25847  degltlem1  26031  ply1rem  26125  fta1blem  26130  ig1pdvds  26139  plyeq0lem  26169  plypf1  26171  plyaddlem1  26172  plymullem1  26173  coemulhi  26213  plycj  26237  plycjOLD  26239  taylfval  26320  abelthlem3  26397  rlimcnp  26929  wilthlem2  27033  logexprlim  27190  2sqreultblem  27413  tgldim0eq  28524  edglnl  29165  nbgr1vtx  29380  vtxdginducedm1lem4  29565  clwlkclwwlklem2a4  30021  eucrct2eupth  30269  frgrncvvdeqlem9  30331  nsnlplig  30505  nsnlpligALT  30506  fsumiunle  32859  cshw1s2  32991  gsumhashmul  33099  xrge0tsmsbi  33105  gsumwrd2dccatlem  33108  cyc3evpm  33181  0ringcring  33283  pidlnz  33406  elrspunidl  33458  0ringprmidl  33479  drngmxidlr  33508  ig1pmindeg  33632  mplmulmvr  33653  vieta  33685  lbslsat  33722  lindsunlem  33730  irngnminplynz  33818  ordtrest2NEW  34029  xrge0iifcnv  34039  xrge0iifhom  34043  esumsnf  34170  esumpr  34172  esumiun  34200  inelpisys  34260  measvunilem0  34319  measvuni  34320  carsggect  34424  omsmeas  34429  plymulx0  34653  repr0  34717  bnj98  34972  bnj1442  35154  bnj1452  35157  subfacp1lem5  35327  erdszelem4  35337  erdszelem8  35341  sconnpi1  35382  cvmlift2lem6  35451  cvmlift2lem12  35457  fmla0xp  35526  onint1  36592  bj-1nel0  37098  bj-sngltag  37127  bj-projval  37140  bj-elsn0  37299  bj-fununsn1  37397  tan2h  37752  lindsenlbs  37755  matunitlindf  37758  ptrest  37759  poimirlem23  37783  poimirlem24  37784  poimirlem25  37785  poimirlem28  37788  poimirlem29  37789  poimirlem30  37790  poimirlem31  37791  poimirlem32  37792  prdsbnd  37933  rrnequiv  37975  grpokerinj  38033  rngoueqz  38080  gidsn  38092  0rngo  38167  isdmn3  38214  dibelval2nd  41351  hdmaprnlem9N  42056  hdmap14lem4a  42070  dvrelog2b  42259  sticksstones11  42349  unitscyglem2  42389  0prjspnrel  42812  hbtlem5  43312  flcidc  43354  safesnsupfiss  43598  frege133d  43948  radcnvrat  44497  unisnALT  45108  sumsnd  45213  fnchoice  45216  rnsnf  45370  founiiun0  45376  elmapsnd  45390  fsneqrn  45397  infxrpnf  45632  supminfxr2  45655  cncfiooicc  46080  fperdvper  46105  dvmptfprodlem  46130  dvnprodlem1  46132  dvnprodlem2  46133  itgcoscmulx  46155  stoweidlem44  46230  fourierdlem49  46341  fourierdlem56  46348  fourierdlem80  46372  fourierdlem93  46385  fourierdlem101  46393  sge00  46562  sge0sn  46565  sge0snmpt  46569  sge0iunmptlemfi  46599  sge0p1  46600  sge0fodjrnlem  46602  sge0snmptf  46623  sge0splitsn  46627  nnfoctbdjlem  46641  meadjiunlem  46651  ismeannd  46653  caratheodorylem1  46712  isomenndlem  46716  hoidmv1le  46780  hoidmvlelem2  46782  hoidmvlelem3  46783  ovnhoilem1  46787  hoiqssbl  46811  ovnovollem1  46842  ovnovollem2  46843  chnerlem1  47068  eldmressn  47225  iccpartltu  47613  sbgoldbo  47975  nnsum3primesprm  47978  bgoldbtbndlem3  47995  stgr1  48149  gpgprismgr4cycllem7  48289  ldepspr  48661  lmod1zr  48681  termcbas2  49669  idfudiag1  49712