Theorem elsni 4608

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sn 4592

This theorem is referenced by:  elsnd  4609  elsn2g  4632  nelsn  4634  elpwunsn  4652  eqoreldif  4653  disjsn2  4680  rabsnifsb  4690  sssn  4793  disjxsn  5104  opth1  5455  sosn  5746  ressn  6283  elsnxp  6289  elsuci  6427  funcnvsn  6583  funopdmsn  7145  fvconst  7158  fnsnr  7159  fmptap  7166  mposnif  7524  resf1extb  7927  1stconst  8091  2ndconst  8092  reldmtpos  8226  tpostpos  8238  disjen  9118  map2xp  9131  en1eqsn  9231  ac6sfi  9240  ixpfi2  9303  elfi2  9370  fisn  9383  unxpwdom2  9546  cantnfp1lem3  9645  djulf1o  9894  djurf1o  9895  djur  9901  eldju2ndl  9906  eldju2ndr  9907  isfin4p1  10295  dcomex  10427  iundom2g  10520  fpwwe2lem12  10623  canthp1lem2  10634  0tsk  10736  elreal2  11113  ax1rid  11142  ltxrlt  11276  un0addcl  12533  un0mulcl  12534  fzodisjsn  13722  elfzonlteqm1  13766  elfzo0l  13781  elfzr  13806  elfzlmr  13807  seqf1o  14075  seqid3  14078  seqz  14082  1exp  14123  hashnn0pnf  14374  hash1elsn  14403  hashprg  14427  cats1un  14754  fsumss  15772  sumsnf  15790  fsumsplitsn  15791  fsum2dlem  15817  fsumcom2  15821  ackbijnn  15878  fprodss  15998  fprod2dlem  16030  fprodcom2  16034  fprodsplitsn  16039  sumeven  16441  sumodd  16442  divalgmod  16460  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  phi1  16828  dfphi2  16829  nnnn0modprm0  16862  ramubcl  17074  0ram  17076  ramz  17081  imasvscafn  17587  mreexmrid  17695  2initoinv  18063  2termoinv  18070  gsumress  18736  gsumval2  18740  smndex1basss  18963  smndex1mndlem  18967  0nsg  19231  symgextf1lem  19486  symgextf1  19487  pmtrprfval  19553  psgnsn  19586  lsmdisj2  19748  subgdisj1  19757  lt6abl  19961  gsumsnfd  20017  gsumzunsnd  20022  gsumunsnfd  20023  gsum2dlem2  20037  dprdfeq0  20090  dprdsn  20104  dprd2da  20110  pgpfac1lem3a  20144  pgpfaclem2  20150  ablsimpnosubgd  20172  c0snmgmhm  20540  0ring01eq  20609  zrinitorngc  20723  lsssn0  21043  lspsneq0  21107  lspdisjb  21224  0ringprmidl  21442  pzriprnglem12  21607  frgpcyg  21688  obselocv  21843  obs2ss  21844  mplcoe5  22156  psdmul  22294  coe1tm  22399  mat0dim0  22589  mat0dimid  22590  mat0dimscm  22591  mat1dimscm  22597  mavmul0g  22675  mdet0pr  22714  mdetunilem9  22742  cramer0  22812  pmatcollpw3fi1lem1  22908  basdif0  23075  ordtbas  23314  ordtrest2  23326  cmpfi  23530  refun0  23637  txdis1cn  23757  ptrescn  23761  txkgen  23774  xkoptsub  23776  ordthmeolem  23923  pt1hmeo  23928  filconn  24005  filufint  24042  flimclslem  24106  ptcmplem3  24176  idnghm  24865  iccpnfcnv  25068  iccpnfhmeo  25069  bndth  25082  ivthicc  25582  ovoliunlem1  25626  i1fima2sn  25804  i1f1  25814  itg1addlem4  25823  itg1addlem5  25824  i1fmulc  25827  limcres  26010  limccnp  26015  limccnp2  26016  degltlem1  26194  ply1rem  26288  fta1blem  26293  ig1pdvds  26302  plyeq0lem  26332  plypf1  26334  plyaddlem1  26335  plymullem1  26336  coemulhi  26376  plycj  26399  plycjOLD  26401  plyn0mulidp  26407  taylfval  26484  abelthlem3  26558  rlimcnp  27092  wilthlem2  27195  logexprlim  27351  2sqreultblem  27574  tgldim0eq  28734  edglnl  29430  nbgr1vtx  29645  vtxdginducedm1lem4  29829  clwlkclwwlklem2a4  30285  eucrct2eupth  30533  frgrncvvdeqlem9  30595  nsnlplig  30770  nsnlpligALT  30771  fsumiunle  33110  cshw1s2  33217  gsumhashmul  33324  xrge0tsmsbi  33331  gsumwrd2dccatlem  33334  cyc3evpm  33407  0ringcring  33509  pidlnz  33629  elrspunidl  33676  drngmxidlr  33701  ig1pmindeg  33833  0mplrim  33845  selvply1rhmlemb  33850  mplmulmvr  33870  vieta  33911  lbslsat  33947  lindsunlem  33955  irngnminplynz  34043  ordtrest2NEW  34254  xrge0iifcnv  34264  xrge0iifhom  34268  esumsnf  34395  esumpr  34397  esumiun  34425  inelpisys  34485  measvunilem0  34544  measvuni  34545  carsggect  34649  omsmeas  34654  repr0  34939  bnj98  35196  bnj1442  35378  bnj1452  35381  subfacp1lem5  35571  erdszelem4  35581  erdszelem8  35585  sconnpi1  35626  cvmlift2lem6  35695  cvmlift2lem12  35701  fmla0xp  35770  onint1  36845  dfttc4lem2  36925  bj-1nel0  37474  bj-sngltag  37503  bj-projval  37516  bj-elsn0  37682  bj-fununsn1  37780  tan2h  38146  lindsenlbs  38149  matunitlindf  38152  ptrest  38153  poimirlem23  38177  poimirlem24  38178  poimirlem25  38179  poimirlem28  38182  poimirlem29  38183  poimirlem30  38184  poimirlem31  38185  poimirlem32  38186  prdsbnd  38327  rrnequiv  38369  grpokerinj  38427  rngoueqz  38474  gidsn  38486  0rngo  38561  isdmn3  38608  dibelval2nd  41811  hdmaprnlem9N  42516  hdmap14lem4a  42530  dvrelog2b  42718  sticksstones11  42808  unitscyglem2  42848  0prjspnrel  43244  hbtlem5  43740  flcidc  43782  safesnsupfiss  44026  frege133d  44376  radcnvrat  44909  unisnALT  45519  sumsnd  45631  fnchoice  45634  rnsnf  45787  founiiun0  45793  elmapsnd  45806  fsneqrn  45812  infxrpnf  46045  supminfxr2  46068  cncfiooicc  46493  fperdvper  46518  dvmptfprodlem  46543  dvnprodlem1  46545  dvnprodlem2  46546  itgcoscmulx  46568  stoweidlem44  46643  fourierdlem49  46754  fourierdlem56  46761  fourierdlem80  46785  fourierdlem93  46798  fourierdlem101  46806  sge00  46975  sge0sn  46978  sge0snmpt  46982  sge0iunmptlemfi  47012  sge0p1  47013  sge0fodjrnlem  47015  sge0snmptf  47036  sge0splitsn  47040  nnfoctbdjlem  47054  meadjiunlem  47064  ismeannd  47066  caratheodorylem1  47125  isomenndlem  47129  hoidmv1le  47193  hoidmvlelem2  47195  hoidmvlelem3  47196  ovnhoilem1  47200  hoiqssbl  47224  ovnovollem1  47255  ovnovollem2  47256  chnerlem1  47483  eldmressn  47656  iccpartltu  48056  sbgoldbo  48434  nnsum3primesprm  48437  bgoldbtbndlem3  48454  stgr1  48608  gpgprismgr4cycllem7  48748  ldepspr  49131  lmod1zr  49151  termcbas2  50138  idfudiag1  50181