Theorem elsni 4590

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {csn 4573

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sn 4574

This theorem is referenced by:  elsnd  4591  elsn2g  4614  nelsn  4616  elpwunsn  4634  eqoreldif  4635  disjsn2  4662  rabsnifsb  4672  sssn  4775  disjxsn  5083  opth1  5413  sosn  5701  ressn  6232  elsnxp  6238  elsuci  6375  funcnvsn  6531  funopdmsn  7083  fvconst  7096  fnsnr  7097  fmptap  7104  mposnif  7462  resf1extb  7864  1stconst  8030  2ndconst  8031  reldmtpos  8164  tpostpos  8176  disjen  9047  map2xp  9060  en1eqsn  9159  ac6sfi  9168  ixpfi2  9234  elfi2  9298  fisn  9311  unxpwdom2  9474  cantnfp1lem3  9570  djulf1o  9805  djurf1o  9806  djur  9812  eldju2ndl  9817  eldju2ndr  9818  isfin4p1  10206  dcomex  10338  iundom2g  10431  fpwwe2lem12  10533  canthp1lem2  10544  0tsk  10646  elreal2  11023  ax1rid  11052  ltxrlt  11183  un0addcl  12414  un0mulcl  12415  fzodisjsn  13597  elfzonlteqm1  13641  elfzo0l  13656  elfzr  13681  elfzlmr  13682  seqf1o  13950  seqid3  13953  seqz  13957  1exp  13998  hashnn0pnf  14249  hash1elsn  14278  hashprg  14302  cats1un  14628  fsumss  15632  sumsnf  15650  fsumsplitsn  15651  fsum2dlem  15677  fsumcom2  15681  ackbijnn  15735  fprodss  15855  fprod2dlem  15887  fprodcom2  15891  fprodsplitsn  15896  sumeven  16298  sumodd  16299  divalgmod  16317  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  phi1  16684  dfphi2  16685  nnnn0modprm0  16718  ramubcl  16930  0ram  16932  ramz  16937  imasvscafn  17441  mreexmrid  17549  2initoinv  17917  2termoinv  17924  gsumress  18590  gsumval2  18594  smndex1basss  18813  smndex1mndlem  18817  0nsg  19081  symgextf1lem  19332  symgextf1  19333  pmtrprfval  19399  psgnsn  19432  lsmdisj2  19594  subgdisj1  19603  lt6abl  19807  gsumsnfd  19863  gsumzunsnd  19868  gsumunsnfd  19869  gsum2dlem2  19883  dprdfeq0  19936  dprdsn  19950  dprd2da  19956  pgpfac1lem3a  19990  pgpfaclem2  19996  ablsimpnosubgd  20018  c0snmgmhm  20380  0ring01eq  20444  zrinitorngc  20557  lsssn0  20881  lspsneq0  20945  lspdisjb  21063  pzriprnglem12  21429  frgpcyg  21510  obselocv  21665  obs2ss  21666  mplcoe5  21975  psdmul  22081  coe1tm  22187  mat0dim0  22382  mat0dimid  22383  mat0dimscm  22384  mat1dimscm  22390  mavmul0g  22468  mdet0pr  22507  mdetunilem9  22535  cramer0  22605  pmatcollpw3fi1lem1  22701  basdif0  22868  ordtbas  23107  ordtrest2  23119  cmpfi  23323  refun0  23430  txdis1cn  23550  ptrescn  23554  txkgen  23567  xkoptsub  23569  ordthmeolem  23716  pt1hmeo  23721  filconn  23798  filufint  23835  flimclslem  23899  ptcmplem3  23969  idnghm  24658  iccpnfcnv  24869  iccpnfhmeo  24870  bndth  24884  ivthicc  25386  ovoliunlem1  25430  i1fima2sn  25608  i1f1  25618  itg1addlem4  25627  itg1addlem5  25628  i1fmulc  25631  limcres  25814  limccnp  25819  limccnp2  25820  degltlem1  26004  ply1rem  26098  fta1blem  26103  ig1pdvds  26112  plyeq0lem  26142  plypf1  26144  plyaddlem1  26145  plymullem1  26146  coemulhi  26186  plycj  26210  plycjOLD  26212  taylfval  26293  abelthlem3  26370  rlimcnp  26902  wilthlem2  27006  logexprlim  27163  2sqreultblem  27386  tgldim0eq  28481  edglnl  29121  nbgr1vtx  29336  vtxdginducedm1lem4  29521  clwlkclwwlklem2a4  29977  eucrct2eupth  30225  frgrncvvdeqlem9  30287  nsnlplig  30461  nsnlpligALT  30462  fsumiunle  32812  cshw1s2  32941  gsumhashmul  33041  xrge0tsmsbi  33043  gsumwrd2dccatlem  33046  cyc3evpm  33119  0ringcring  33219  pidlnz  33341  elrspunidl  33393  0ringprmidl  33414  drngmxidlr  33443  ig1pmindeg  33562  lbslsat  33629  lindsunlem  33637  irngnminplynz  33725  ordtrest2NEW  33936  xrge0iifcnv  33946  xrge0iifhom  33950  esumsnf  34077  esumpr  34079  esumiun  34107  inelpisys  34167  measvunilem0  34226  measvuni  34227  carsggect  34331  omsmeas  34336  plymulx0  34560  repr0  34624  bnj98  34879  bnj1442  35061  bnj1452  35064  subfacp1lem5  35228  erdszelem4  35238  erdszelem8  35242  sconnpi1  35283  cvmlift2lem6  35352  cvmlift2lem12  35358  fmla0xp  35427  onint1  36493  bj-1nel0  36998  bj-sngltag  37027  bj-projval  37040  bj-elsn0  37199  bj-fununsn1  37297  tan2h  37662  lindsenlbs  37665  matunitlindf  37668  ptrest  37669  poimirlem23  37693  poimirlem24  37694  poimirlem25  37695  poimirlem28  37698  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  prdsbnd  37843  rrnequiv  37885  grpokerinj  37943  rngoueqz  37990  gidsn  38002  0rngo  38077  isdmn3  38124  dibelval2nd  41261  hdmaprnlem9N  41966  hdmap14lem4a  41980  dvrelog2b  42169  sticksstones11  42259  unitscyglem2  42299  0prjspnrel  42730  hbtlem5  43231  flcidc  43273  safesnsupfiss  43518  frege133d  43868  radcnvrat  44417  unisnALT  45028  sumsnd  45133  fnchoice  45136  rnsnf  45291  founiiun0  45297  elmapsnd  45311  fsneqrn  45318  infxrpnf  45554  supminfxr2  45577  cncfiooicc  46002  fperdvper  46027  dvmptfprodlem  46052  dvnprodlem1  46054  dvnprodlem2  46055  itgcoscmulx  46077  stoweidlem44  46152  fourierdlem49  46263  fourierdlem56  46270  fourierdlem80  46294  fourierdlem93  46307  fourierdlem101  46315  sge00  46484  sge0sn  46487  sge0snmpt  46491  sge0iunmptlemfi  46521  sge0p1  46522  sge0fodjrnlem  46524  sge0snmptf  46545  sge0splitsn  46549  nnfoctbdjlem  46563  meadjiunlem  46573  ismeannd  46575  caratheodorylem1  46634  isomenndlem  46638  hoidmv1le  46702  hoidmvlelem2  46704  hoidmvlelem3  46705  ovnhoilem1  46709  hoiqssbl  46733  ovnovollem1  46764  ovnovollem2  46765  chnerlem1  46990  eldmressn  47147  iccpartltu  47535  sbgoldbo  47897  nnsum3primesprm  47900  bgoldbtbndlem3  47917  stgr1  48071  gpgprismgr4cycllem7  48211  ldepspr  48584  lmod1zr  48604  termcbas2  49593  idfudiag1  49636