Theorem elsni 4575

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sn 4559

This theorem is referenced by:  elsn2g  4596  nelsn  4598  elpwunsn  4616  eqoreldif  4617  disjsn2  4645  rabsnifsb  4655  sssn  4756  disjxsn  5063  opth1  5384  sosn  5664  ressn  6177  elsnxp  6183  elsuci  6317  funcnvsn  6468  funopdmsn  7004  fvconst  7018  fnsnr  7019  fmptap  7024  mposnif  7368  1stconst  7911  2ndconst  7912  reldmtpos  8021  tpostpos  8033  disjen  8870  map2xp  8883  ac6sfi  8988  ixpfi2  9047  elfi2  9103  fisn  9116  unxpwdom2  9277  cantnfp1lem3  9368  djulf1o  9601  djurf1o  9602  djur  9608  eldju2ndl  9613  eldju2ndr  9614  isfin4p1  10002  dcomex  10134  iundom2g  10227  fpwwe2lem12  10329  canthp1lem2  10340  0tsk  10442  elreal2  10819  ax1rid  10848  ltxrlt  10976  un0addcl  12196  un0mulcl  12197  fzodisjsn  13353  elfzonlteqm1  13391  elfzo0l  13405  elfzr  13428  elfzlmr  13429  seqf1o  13692  seqid3  13695  seqz  13699  1exp  13740  hashnn0pnf  13984  hash1elsn  14014  hashprg  14038  cats1un  14362  fsumss  15365  sumsnf  15383  fsumsplitsn  15384  fsum2dlem  15410  fsumcom2  15414  ackbijnn  15468  fprodss  15586  fprod2dlem  15618  fprodcom2  15622  fprodsplitsn  15627  sumeven  16024  sumodd  16025  divalgmod  16043  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  phi1  16402  dfphi2  16403  nnnn0modprm0  16435  ramubcl  16647  0ram  16649  ramz  16654  imasvscafn  17165  mreexmrid  17269  2initoinv  17641  2termoinv  17648  gsumress  18281  gsumval2  18285  smndex1basss  18459  smndex1mndlem  18463  0nsg  18712  symgextf1lem  18943  symgextf1  18944  pmtrprfval  19010  psgnsn  19043  lsmdisj2  19203  subgdisj1  19212  lt6abl  19411  gsumsnfd  19467  gsumzunsnd  19472  gsumunsnfd  19473  gsum2dlem2  19487  dprdfeq0  19540  dprdsn  19554  dprd2da  19560  pgpfac1lem3a  19594  pgpfaclem2  19600  ablsimpnosubgd  19622  lsssn0  20124  lspsneq0  20189  lspdisjb  20303  0ring01eq  20455  frgpcyg  20693  obselocv  20845  obs2ss  20846  mplcoe5  21151  coe1tm  21354  mat0dim0  21524  mat0dimid  21525  mat0dimscm  21526  mat1dimscm  21532  mavmul0g  21610  mdet0pr  21649  mdetunilem9  21677  cramer0  21747  pmatcollpw3fi1lem1  21843  basdif0  22011  ordtbas  22251  ordtrest2  22263  cmpfi  22467  refun0  22574  txdis1cn  22694  ptrescn  22698  txkgen  22711  xkoptsub  22713  ordthmeolem  22860  pt1hmeo  22865  filconn  22942  filufint  22979  flimclslem  23043  ptcmplem3  23113  idnghm  23813  iccpnfcnv  24013  iccpnfhmeo  24014  bndth  24027  ivthicc  24527  ovoliunlem1  24571  i1fima2sn  24749  i1f1  24759  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  i1fmulc  24773  limcres  24955  limccnp  24960  limccnp2  24961  degltlem1  25142  ply1rem  25233  fta1blem  25238  ig1pdvds  25246  plyeq0lem  25276  plypf1  25278  plyaddlem1  25279  plymullem1  25280  coemulhi  25320  plycj  25343  taylfval  25423  abelthlem3  25497  rlimcnp  26020  wilthlem2  26123  logexprlim  26278  2sqreultblem  26501  tgldim0eq  26768  edglnl  27416  nbgr1vtx  27628  vtxdginducedm1lem4  27812  clwlkclwwlklem2a4  28262  eucrct2eupth  28510  frgrncvvdeqlem9  28572  nsnlplig  28744  nsnlpligALT  28745  fsumiunle  31045  cshw1s2  31134  gsumhashmul  31218  xrge0tsmsbi  31220  cyc3evpm  31319  pidlnz  31473  elrspunidl  31508  0ringprmidl  31527  lbslsat  31601  lindsunlem  31607  ordtrest2NEW  31775  xrge0iifcnv  31785  xrge0iifhom  31789  esumsnf  31932  esumpr  31934  esumiun  31962  inelpisys  32022  measvunilem0  32081  measvuni  32082  carsggect  32185  omsmeas  32190  plymulx0  32426  repr0  32491  bnj98  32747  bnj1442  32929  bnj1452  32932  subfacp1lem5  33046  erdszelem4  33056  erdszelem8  33060  sconnpi1  33101  cvmlift2lem6  33170  cvmlift2lem12  33176  fmla0xp  33245  onint1  34565  bj-1nel0  35071  bj-sngltag  35100  bj-projval  35113  bj-elsn0  35253  bj-fununsn1  35351  tan2h  35696  lindsenlbs  35699  matunitlindf  35702  ptrest  35703  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  prdsbnd  35878  rrnequiv  35920  grpokerinj  35978  rngoueqz  36025  gidsn  36037  0rngo  36112  isdmn3  36159  dibelval2nd  39093  hdmaprnlem9N  39798  hdmap14lem4a  39812  dvrelog2b  40002  sticksstones11  40040  0prjspnrel  40385  hbtlem5  40869  flcidc  40915  frege133d  41262  radcnvrat  41821  unisnALT  42435  sumsnd  42458  fnchoice  42461  rnsnf  42610  founiiun0  42617  elmapsnd  42633  fsneqrn  42640  infxrpnf  42876  supminfxr2  42899  cncfiooicc  43325  fperdvper  43350  dvmptfprodlem  43375  dvnprodlem1  43377  dvnprodlem2  43378  itgcoscmulx  43400  stoweidlem44  43475  fourierdlem49  43586  fourierdlem56  43593  fourierdlem80  43617  fourierdlem93  43630  fourierdlem101  43638  sge00  43804  sge0sn  43807  sge0snmpt  43811  sge0iunmptlemfi  43841  sge0p1  43842  sge0fodjrnlem  43844  sge0snmptf  43865  sge0splitsn  43869  nnfoctbdjlem  43883  meadjiunlem  43893  ismeannd  43895  caratheodorylem1  43954  isomenndlem  43958  hoidmv1le  44022  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  hoiqssbl  44053  ovnovollem1  44084  ovnovollem2  44085  eldmressn  44418  iccpartltu  44765  sbgoldbo  45127  nnsum3primesprm  45130  bgoldbtbndlem3  45147  c0snmgmhm  45360  zrinitorngc  45446  ldepspr  45702  lmod1zr  45722