Theorem elsni 4647

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sn 4631

This theorem is referenced by:  elsn2g  4668  nelsn  4670  elpwunsn  4688  eqoreldif  4689  disjsn2  4716  rabsnifsb  4726  sssn  4830  disjxsn  5141  opth1  5485  sosn  5774  ressn  6306  elsnxp  6312  elsuci  6452  funcnvsn  6617  funopdmsn  7169  fvconst  7183  fnsnr  7184  fmptap  7189  mposnif  7548  1stconst  8123  2ndconst  8124  reldmtpos  8257  tpostpos  8269  disjen  9172  map2xp  9185  en1eqsn  9305  ac6sfi  9317  ixpfi2  9387  elfi2  9451  fisn  9464  unxpwdom2  9625  cantnfp1lem3  9717  djulf1o  9949  djurf1o  9950  djur  9956  eldju2ndl  9961  eldju2ndr  9962  isfin4p1  10352  dcomex  10484  iundom2g  10577  fpwwe2lem12  10679  canthp1lem2  10690  0tsk  10792  elreal2  11169  ax1rid  11198  ltxrlt  11328  un0addcl  12556  un0mulcl  12557  fzodisjsn  13733  elfzonlteqm1  13776  elfzo0l  13791  elfzr  13815  elfzlmr  13816  seqf1o  14080  seqid3  14083  seqz  14087  1exp  14128  hashnn0pnf  14377  hash1elsn  14406  hashprg  14430  cats1un  14755  fsumss  15757  sumsnf  15775  fsumsplitsn  15776  fsum2dlem  15802  fsumcom2  15806  ackbijnn  15860  fprodss  15980  fprod2dlem  16012  fprodcom2  16016  fprodsplitsn  16021  sumeven  16420  sumodd  16421  divalgmod  16439  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  phi1  16806  dfphi2  16807  nnnn0modprm0  16839  ramubcl  17051  0ram  17053  ramz  17058  imasvscafn  17583  mreexmrid  17687  2initoinv  18063  2termoinv  18070  gsumress  18707  gsumval2  18711  smndex1basss  18930  smndex1mndlem  18934  0nsg  19199  symgextf1lem  19452  symgextf1  19453  pmtrprfval  19519  psgnsn  19552  lsmdisj2  19714  subgdisj1  19723  lt6abl  19927  gsumsnfd  19983  gsumzunsnd  19988  gsumunsnfd  19989  gsum2dlem2  20003  dprdfeq0  20056  dprdsn  20070  dprd2da  20076  pgpfac1lem3a  20110  pgpfaclem2  20116  ablsimpnosubgd  20138  c0snmgmhm  20478  0ring01eq  20545  zrinitorngc  20658  lsssn0  20963  lspsneq0  21027  lspdisjb  21145  pzriprnglem12  21520  frgpcyg  21609  obselocv  21765  obs2ss  21766  mplcoe5  22075  psdmul  22187  coe1tm  22291  mat0dim0  22488  mat0dimid  22489  mat0dimscm  22490  mat1dimscm  22496  mavmul0g  22574  mdet0pr  22613  mdetunilem9  22641  cramer0  22711  pmatcollpw3fi1lem1  22807  basdif0  22975  ordtbas  23215  ordtrest2  23227  cmpfi  23431  refun0  23538  txdis1cn  23658  ptrescn  23662  txkgen  23675  xkoptsub  23677  ordthmeolem  23824  pt1hmeo  23829  filconn  23906  filufint  23943  flimclslem  24007  ptcmplem3  24077  idnghm  24779  iccpnfcnv  24988  iccpnfhmeo  24989  bndth  25003  ivthicc  25506  ovoliunlem1  25550  i1fima2sn  25728  i1f1  25738  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  i1fmulc  25752  limcres  25935  limccnp  25940  limccnp2  25941  degltlem1  26125  ply1rem  26219  fta1blem  26224  ig1pdvds  26233  plyeq0lem  26263  plypf1  26265  plyaddlem1  26266  plymullem1  26267  coemulhi  26307  plycj  26331  plycjOLD  26333  taylfval  26414  abelthlem3  26491  rlimcnp  27022  wilthlem2  27126  logexprlim  27283  2sqreultblem  27506  tgldim0eq  28525  edglnl  29174  nbgr1vtx  29389  vtxdginducedm1lem4  29574  clwlkclwwlklem2a4  30025  eucrct2eupth  30273  frgrncvvdeqlem9  30335  nsnlplig  30509  nsnlpligALT  30510  fsumiunle  32835  cshw1s2  32929  gsumhashmul  33046  xrge0tsmsbi  33048  gsumwrd2dccatlem  33051  cyc3evpm  33152  0ringcring  33238  pidlnz  33383  elrspunidl  33435  0ringprmidl  33456  drngmxidlr  33485  ig1pmindeg  33601  lbslsat  33643  lindsunlem  33651  irngnminplynz  33719  ordtrest2NEW  33883  xrge0iifcnv  33893  xrge0iifhom  33897  esumsnf  34044  esumpr  34046  esumiun  34074  inelpisys  34134  measvunilem0  34193  measvuni  34194  carsggect  34299  omsmeas  34304  plymulx0  34540  repr0  34604  bnj98  34859  bnj1442  35041  bnj1452  35044  subfacp1lem5  35168  erdszelem4  35178  erdszelem8  35182  sconnpi1  35223  cvmlift2lem6  35292  cvmlift2lem12  35298  fmla0xp  35367  onint1  36431  bj-1nel0  36936  bj-sngltag  36965  bj-projval  36978  bj-elsn0  37137  bj-fununsn1  37235  tan2h  37598  lindsenlbs  37601  matunitlindf  37604  ptrest  37605  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem28  37634  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  prdsbnd  37779  rrnequiv  37821  grpokerinj  37879  rngoueqz  37926  gidsn  37938  0rngo  38013  isdmn3  38060  dibelval2nd  41134  hdmaprnlem9N  41839  hdmap14lem4a  41853  dvrelog2b  42047  sticksstones11  42137  unitscyglem2  42177  0prjspnrel  42613  hbtlem5  43116  flcidc  43158  safesnsupfiss  43404  frege133d  43754  radcnvrat  44309  unisnALT  44923  sumsnd  44963  fnchoice  44966  rnsnf  45126  founiiun0  45132  elmapsnd  45146  fsneqrn  45153  infxrpnf  45395  supminfxr2  45418  cncfiooicc  45849  fperdvper  45874  dvmptfprodlem  45899  dvnprodlem1  45901  dvnprodlem2  45902  itgcoscmulx  45924  stoweidlem44  45999  fourierdlem49  46110  fourierdlem56  46117  fourierdlem80  46141  fourierdlem93  46154  fourierdlem101  46162  sge00  46331  sge0sn  46334  sge0snmpt  46338  sge0iunmptlemfi  46368  sge0p1  46369  sge0fodjrnlem  46371  sge0snmptf  46392  sge0splitsn  46396  nnfoctbdjlem  46410  meadjiunlem  46420  ismeannd  46422  caratheodorylem1  46481  isomenndlem  46485  hoidmv1le  46549  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem1  46556  hoiqssbl  46580  ovnovollem1  46611  ovnovollem2  46612  eldmressn  46986  iccpartltu  47349  sbgoldbo  47711  nnsum3primesprm  47714  bgoldbtbndlem3  47731  stgr1  47863  ldepspr  48318  lmod1zr  48338