Theorem elsni 4572

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-sn 4556

This theorem is referenced by:  elsnd  4573  elsn2g  4596  nelsn  4598  elpwunsn  4616  eqoreldif  4617  disjsn2  4644  rabsnifsb  4654  sssn  4757  disjxsn  5066  opth1  5415  sosn  5705  ressn  6236  elsnxp  6242  elsuci  6379  funcnvsn  6535  funopdmsn  7093  fvconst  7106  fnsnr  7107  fmptap  7114  mposnif  7472  resf1extb  7874  1stconst  8039  2ndconst  8040  reldmtpos  8174  tpostpos  8186  disjen  9062  map2xp  9075  en1eqsn  9175  ac6sfi  9184  ixpfi2  9250  elfi2  9317  fisn  9330  unxpwdom2  9493  cantnfp1lem3  9592  djulf1o  9827  djurf1o  9828  djur  9834  eldju2ndl  9839  eldju2ndr  9840  isfin4p1  10228  dcomex  10360  iundom2g  10453  fpwwe2lem12  10556  canthp1lem2  10567  0tsk  10669  elreal2  11046  ax1rid  11075  ltxrlt  11207  un0addcl  12461  un0mulcl  12462  fzodisjsn  13643  elfzonlteqm1  13687  elfzo0l  13702  elfzr  13727  elfzlmr  13728  seqf1o  13996  seqid3  13999  seqz  14003  1exp  14044  hashnn0pnf  14295  hash1elsn  14324  hashprg  14348  cats1un  14674  fsumss  15678  sumsnf  15696  fsumsplitsn  15697  fsum2dlem  15723  fsumcom2  15727  ackbijnn  15784  fprodss  15904  fprod2dlem  15936  fprodcom2  15940  fprodsplitsn  15945  sumeven  16347  sumodd  16348  divalgmod  16366  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  phi1  16734  dfphi2  16735  nnnn0modprm0  16768  ramubcl  16980  0ram  16982  ramz  16987  imasvscafn  17492  mreexmrid  17600  2initoinv  17968  2termoinv  17975  gsumress  18641  gsumval2  18645  smndex1basss  18867  smndex1mndlem  18871  0nsg  19135  symgextf1lem  19386  symgextf1  19387  pmtrprfval  19453  psgnsn  19486  lsmdisj2  19648  subgdisj1  19657  lt6abl  19861  gsumsnfd  19917  gsumzunsnd  19922  gsumunsnfd  19923  gsum2dlem2  19937  dprdfeq0  19990  dprdsn  20004  dprd2da  20010  pgpfac1lem3a  20044  pgpfaclem2  20050  ablsimpnosubgd  20072  c0snmgmhm  20433  0ring01eq  20501  zrinitorngc  20614  lsssn0  20938  lspsneq0  21002  lspdisjb  21119  pzriprnglem12  21467  frgpcyg  21548  obselocv  21703  obs2ss  21704  mplcoe5  22016  psdmul  22154  coe1tm  22259  mat0dim0  22450  mat0dimid  22451  mat0dimscm  22452  mat1dimscm  22458  mavmul0g  22536  mdet0pr  22575  mdetunilem9  22603  cramer0  22673  pmatcollpw3fi1lem1  22769  basdif0  22936  ordtbas  23175  ordtrest2  23187  cmpfi  23391  refun0  23498  txdis1cn  23618  ptrescn  23622  txkgen  23635  xkoptsub  23637  ordthmeolem  23784  pt1hmeo  23789  filconn  23866  filufint  23903  flimclslem  23967  ptcmplem3  24037  idnghm  24726  iccpnfcnv  24929  iccpnfhmeo  24930  bndth  24943  ivthicc  25443  ovoliunlem1  25487  i1fima2sn  25665  i1f1  25675  itg1addlem4  25684  itg1addlem5  25685  i1fmulc  25688  limcres  25871  limccnp  25876  limccnp2  25877  degltlem1  26055  ply1rem  26149  fta1blem  26154  ig1pdvds  26163  plyeq0lem  26193  plypf1  26195  plyaddlem1  26196  plymullem1  26197  coemulhi  26237  plycj  26260  plycjOLD  26262  taylfval  26342  abelthlem3  26416  rlimcnp  26947  wilthlem2  27050  logexprlim  27206  2sqreultblem  27429  tgldim0eq  28589  edglnl  29230  nbgr1vtx  29445  vtxdginducedm1lem4  29629  clwlkclwwlklem2a4  30085  eucrct2eupth  30333  frgrncvvdeqlem9  30395  nsnlplig  30570  nsnlpligALT  30571  fsumiunle  32921  cshw1s2  33039  gsumhashmul  33148  xrge0tsmsbi  33155  gsumwrd2dccatlem  33158  cyc3evpm  33231  0ringcring  33333  pidlnz  33459  elrspunidl  33511  0ringprmidl  33532  drngmxidlr  33561  ig1pmindeg  33685  0mplrim  33698  selvply1rhmlemb  33703  mplmulmvr  33723  vieta  33764  lbslsat  33800  lindsunlem  33808  irngnminplynz  33896  ordtrest2NEW  34107  xrge0iifcnv  34117  xrge0iifhom  34121  esumsnf  34248  esumpr  34250  esumiun  34278  inelpisys  34338  measvunilem0  34397  measvuni  34398  carsggect  34502  omsmeas  34507  plymulx0  34731  repr0  34795  bnj98  35049  bnj1442  35231  bnj1452  35234  subfacp1lem5  35412  erdszelem4  35422  erdszelem8  35426  sconnpi1  35467  cvmlift2lem6  35536  cvmlift2lem12  35542  fmla0xp  35611  onint1  36677  dfttc4lem2  36757  bj-1nel0  37307  bj-sngltag  37336  bj-projval  37349  bj-elsn0  37515  bj-fununsn1  37613  tan2h  37979  lindsenlbs  37982  matunitlindf  37985  ptrest  37986  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem28  38015  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  prdsbnd  38160  rrnequiv  38202  grpokerinj  38260  rngoueqz  38307  gidsn  38319  0rngo  38394  isdmn3  38441  dibelval2nd  41644  hdmaprnlem9N  42349  hdmap14lem4a  42363  dvrelog2b  42551  sticksstones11  42641  unitscyglem2  42681  0prjspnrel  43077  hbtlem5  43573  flcidc  43615  safesnsupfiss  43859  frege133d  44209  radcnvrat  44758  unisnALT  45369  sumsnd  45474  fnchoice  45477  rnsnf  45631  founiiun0  45637  elmapsnd  45650  fsneqrn  45656  infxrpnf  45889  supminfxr2  45912  cncfiooicc  46337  fperdvper  46362  dvmptfprodlem  46387  dvnprodlem1  46389  dvnprodlem2  46390  itgcoscmulx  46412  stoweidlem44  46487  fourierdlem49  46598  fourierdlem56  46605  fourierdlem80  46629  fourierdlem93  46642  fourierdlem101  46650  sge00  46819  sge0sn  46822  sge0snmpt  46826  sge0iunmptlemfi  46856  sge0p1  46857  sge0fodjrnlem  46859  sge0snmptf  46880  sge0splitsn  46884  nnfoctbdjlem  46898  meadjiunlem  46908  ismeannd  46910  caratheodorylem1  46969  isomenndlem  46973  hoidmv1le  47037  hoidmvlelem2  47039  hoidmvlelem3  47040  ovnhoilem1  47044  hoiqssbl  47068  ovnovollem1  47099  ovnovollem2  47100  chnerlem1  47327  eldmressn  47500  iccpartltu  47900  sbgoldbo  48278  nnsum3primesprm  48281  bgoldbtbndlem3  48298  stgr1  48452  gpgprismgr4cycllem7  48592  ldepspr  48964  lmod1zr  48984  termcbas2  49972  idfudiag1  50015