Theorem elsni 4645

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sn 4629

This theorem is referenced by:  elsn2g  4666  nelsn  4668  elpwunsn  4687  eqoreldif  4688  disjsn2  4716  rabsnifsb  4726  sssn  4829  disjxsn  5141  opth1  5475  sosn  5761  ressn  6282  elsnxp  6288  elsuci  6429  funcnvsn  6596  funopdmsn  7145  fvconst  7159  fnsnr  7160  fmptap  7165  mposnif  7521  1stconst  8083  2ndconst  8084  reldmtpos  8216  tpostpos  8228  disjen  9131  map2xp  9144  en1eqsn  9271  ac6sfi  9284  ixpfi2  9347  elfi2  9406  fisn  9419  unxpwdom2  9580  cantnfp1lem3  9672  djulf1o  9904  djurf1o  9905  djur  9911  eldju2ndl  9916  eldju2ndr  9917  isfin4p1  10307  dcomex  10439  iundom2g  10532  fpwwe2lem12  10634  canthp1lem2  10645  0tsk  10747  elreal2  11124  ax1rid  11153  ltxrlt  11281  un0addcl  12502  un0mulcl  12503  fzodisjsn  13667  elfzonlteqm1  13705  elfzo0l  13719  elfzr  13742  elfzlmr  13743  seqf1o  14006  seqid3  14009  seqz  14013  1exp  14054  hashnn0pnf  14299  hash1elsn  14328  hashprg  14352  cats1un  14668  fsumss  15668  sumsnf  15686  fsumsplitsn  15687  fsum2dlem  15713  fsumcom2  15717  ackbijnn  15771  fprodss  15889  fprod2dlem  15921  fprodcom2  15925  fprodsplitsn  15930  sumeven  16327  sumodd  16328  divalgmod  16346  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  phi1  16703  dfphi2  16704  nnnn0modprm0  16736  ramubcl  16948  0ram  16950  ramz  16955  imasvscafn  17480  mreexmrid  17584  2initoinv  17957  2termoinv  17964  gsumress  18598  gsumval2  18602  smndex1basss  18783  smndex1mndlem  18787  0nsg  19044  symgextf1lem  19283  symgextf1  19284  pmtrprfval  19350  psgnsn  19383  lsmdisj2  19545  subgdisj1  19554  lt6abl  19758  gsumsnfd  19814  gsumzunsnd  19819  gsumunsnfd  19820  gsum2dlem2  19834  dprdfeq0  19887  dprdsn  19901  dprd2da  19907  pgpfac1lem3a  19941  pgpfaclem2  19947  ablsimpnosubgd  19969  0ring01eq  20297  lsssn0  20551  lspsneq0  20616  lspdisjb  20732  frgpcyg  21121  obselocv  21275  obs2ss  21276  mplcoe5  21587  coe1tm  21787  mat0dim0  21961  mat0dimid  21962  mat0dimscm  21963  mat1dimscm  21969  mavmul0g  22047  mdet0pr  22086  mdetunilem9  22114  cramer0  22184  pmatcollpw3fi1lem1  22280  basdif0  22448  ordtbas  22688  ordtrest2  22700  cmpfi  22904  refun0  23011  txdis1cn  23131  ptrescn  23135  txkgen  23148  xkoptsub  23150  ordthmeolem  23297  pt1hmeo  23302  filconn  23379  filufint  23416  flimclslem  23480  ptcmplem3  23550  idnghm  24252  iccpnfcnv  24452  iccpnfhmeo  24453  bndth  24466  ivthicc  24967  ovoliunlem1  25011  i1fima2sn  25189  i1f1  25199  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  i1fmulc  25213  limcres  25395  limccnp  25400  limccnp2  25401  degltlem1  25582  ply1rem  25673  fta1blem  25678  ig1pdvds  25686  plyeq0lem  25716  plypf1  25718  plyaddlem1  25719  plymullem1  25720  coemulhi  25760  plycj  25783  taylfval  25863  abelthlem3  25937  rlimcnp  26460  wilthlem2  26563  logexprlim  26718  2sqreultblem  26941  tgldim0eq  27744  edglnl  28393  nbgr1vtx  28605  vtxdginducedm1lem4  28789  clwlkclwwlklem2a4  29240  eucrct2eupth  29488  frgrncvvdeqlem9  29550  nsnlplig  29722  nsnlpligALT  29723  fsumiunle  32023  cshw1s2  32112  gsumhashmul  32196  xrge0tsmsbi  32198  cyc3evpm  32297  pidlnz  32477  elrspunidl  32535  0ringprmidl  32557  ig1pmindeg  32660  lbslsat  32690  lindsunlem  32698  irngnminplynz  32760  ordtrest2NEW  32892  xrge0iifcnv  32902  xrge0iifhom  32906  esumsnf  33051  esumpr  33053  esumiun  33081  inelpisys  33141  measvunilem0  33200  measvuni  33201  carsggect  33306  omsmeas  33311  plymulx0  33547  repr0  33612  bnj98  33867  bnj1442  34049  bnj1452  34052  subfacp1lem5  34164  erdszelem4  34174  erdszelem8  34178  sconnpi1  34219  cvmlift2lem6  34288  cvmlift2lem12  34294  fmla0xp  34363  onint1  35323  bj-1nel0  35824  bj-sngltag  35853  bj-projval  35866  bj-elsn0  36025  bj-fununsn1  36123  tan2h  36469  lindsenlbs  36472  matunitlindf  36475  ptrest  36476  poimirlem23  36500  poimirlem24  36501  poimirlem25  36502  poimirlem28  36505  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimirlem32  36509  prdsbnd  36650  rrnequiv  36692  grpokerinj  36750  rngoueqz  36797  gidsn  36809  0rngo  36884  isdmn3  36931  dibelval2nd  40012  hdmaprnlem9N  40717  hdmap14lem4a  40731  dvrelog2b  40920  sticksstones11  40961  0prjspnrel  41366  hbtlem5  41856  flcidc  41902  safesnsupfiss  42152  frege133d  42502  radcnvrat  43059  unisnALT  43673  sumsnd  43696  fnchoice  43699  rnsnf  43867  founiiun0  43874  elmapsnd  43889  fsneqrn  43896  infxrpnf  44143  supminfxr2  44166  cncfiooicc  44597  fperdvper  44622  dvmptfprodlem  44647  dvnprodlem1  44649  dvnprodlem2  44650  itgcoscmulx  44672  stoweidlem44  44747  fourierdlem49  44858  fourierdlem56  44865  fourierdlem80  44889  fourierdlem93  44902  fourierdlem101  44910  sge00  45079  sge0sn  45082  sge0snmpt  45086  sge0iunmptlemfi  45116  sge0p1  45117  sge0fodjrnlem  45119  sge0snmptf  45140  sge0splitsn  45144  nnfoctbdjlem  45158  meadjiunlem  45168  ismeannd  45170  caratheodorylem1  45229  isomenndlem  45233  hoidmv1le  45297  hoidmvlelem2  45299  hoidmvlelem3  45300  ovnhoilem1  45304  hoiqssbl  45328  ovnovollem1  45359  ovnovollem2  45360  eldmressn  45734  iccpartltu  46080  sbgoldbo  46442  nnsum3primesprm  46445  bgoldbtbndlem3  46462  c0snmgmhm  46699  zrinitorngc  46852  ldepspr  47108  lmod1zr  47128