Theorem elsni 4646

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

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

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 4630

This theorem is referenced by:  elsn2g  4667  nelsn  4669  elpwunsn  4688  eqoreldif  4689  disjsn2  4717  rabsnifsb  4727  sssn  4830  disjxsn  5142  opth1  5476  sosn  5763  ressn  6285  elsnxp  6291  elsuci  6432  funcnvsn  6599  funopdmsn  7148  fvconst  7162  fnsnr  7163  fmptap  7168  mposnif  7524  1stconst  8086  2ndconst  8087  reldmtpos  8219  tpostpos  8231  disjen  9134  map2xp  9147  en1eqsn  9274  ac6sfi  9287  ixpfi2  9350  elfi2  9409  fisn  9422  unxpwdom2  9583  cantnfp1lem3  9675  djulf1o  9907  djurf1o  9908  djur  9914  eldju2ndl  9919  eldju2ndr  9920  isfin4p1  10310  dcomex  10442  iundom2g  10535  fpwwe2lem12  10637  canthp1lem2  10648  0tsk  10750  elreal2  11127  ax1rid  11156  ltxrlt  11284  un0addcl  12505  un0mulcl  12506  fzodisjsn  13670  elfzonlteqm1  13708  elfzo0l  13722  elfzr  13745  elfzlmr  13746  seqf1o  14009  seqid3  14012  seqz  14016  1exp  14057  hashnn0pnf  14302  hash1elsn  14331  hashprg  14355  cats1un  14671  fsumss  15671  sumsnf  15689  fsumsplitsn  15690  fsum2dlem  15716  fsumcom2  15720  ackbijnn  15774  fprodss  15892  fprod2dlem  15924  fprodcom2  15928  fprodsplitsn  15933  sumeven  16330  sumodd  16331  divalgmod  16349  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  phi1  16706  dfphi2  16707  nnnn0modprm0  16739  ramubcl  16951  0ram  16953  ramz  16958  imasvscafn  17483  mreexmrid  17587  2initoinv  17960  2termoinv  17967  gsumress  18601  gsumval2  18605  smndex1basss  18786  smndex1mndlem  18790  0nsg  19049  symgextf1lem  19288  symgextf1  19289  pmtrprfval  19355  psgnsn  19388  lsmdisj2  19550  subgdisj1  19559  lt6abl  19763  gsumsnfd  19819  gsumzunsnd  19824  gsumunsnfd  19825  gsum2dlem2  19839  dprdfeq0  19892  dprdsn  19906  dprd2da  19912  pgpfac1lem3a  19946  pgpfaclem2  19952  ablsimpnosubgd  19974  0ring01eq  20304  lsssn0  20558  lspsneq0  20623  lspdisjb  20739  frgpcyg  21129  obselocv  21283  obs2ss  21284  mplcoe5  21595  coe1tm  21795  mat0dim0  21969  mat0dimid  21970  mat0dimscm  21971  mat1dimscm  21977  mavmul0g  22055  mdet0pr  22094  mdetunilem9  22122  cramer0  22192  pmatcollpw3fi1lem1  22288  basdif0  22456  ordtbas  22696  ordtrest2  22708  cmpfi  22912  refun0  23019  txdis1cn  23139  ptrescn  23143  txkgen  23156  xkoptsub  23158  ordthmeolem  23305  pt1hmeo  23310  filconn  23387  filufint  23424  flimclslem  23488  ptcmplem3  23558  idnghm  24260  iccpnfcnv  24460  iccpnfhmeo  24461  bndth  24474  ivthicc  24975  ovoliunlem1  25019  i1fima2sn  25197  i1f1  25207  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  i1fmulc  25221  limcres  25403  limccnp  25408  limccnp2  25409  degltlem1  25590  ply1rem  25681  fta1blem  25686  ig1pdvds  25694  plyeq0lem  25724  plypf1  25726  plyaddlem1  25727  plymullem1  25728  coemulhi  25768  plycj  25791  taylfval  25871  abelthlem3  25945  rlimcnp  26470  wilthlem2  26573  logexprlim  26728  2sqreultblem  26951  tgldim0eq  27754  edglnl  28403  nbgr1vtx  28615  vtxdginducedm1lem4  28799  clwlkclwwlklem2a4  29250  eucrct2eupth  29498  frgrncvvdeqlem9  29560  nsnlplig  29734  nsnlpligALT  29735  fsumiunle  32035  cshw1s2  32124  gsumhashmul  32208  xrge0tsmsbi  32210  cyc3evpm  32309  pidlnz  32488  elrspunidl  32546  0ringprmidl  32568  ig1pmindeg  32671  lbslsat  32701  lindsunlem  32709  irngnminplynz  32771  ordtrest2NEW  32903  xrge0iifcnv  32913  xrge0iifhom  32917  esumsnf  33062  esumpr  33064  esumiun  33092  inelpisys  33152  measvunilem0  33211  measvuni  33212  carsggect  33317  omsmeas  33322  plymulx0  33558  repr0  33623  bnj98  33878  bnj1442  34060  bnj1452  34063  subfacp1lem5  34175  erdszelem4  34185  erdszelem8  34189  sconnpi1  34230  cvmlift2lem6  34299  cvmlift2lem12  34305  fmla0xp  34374  onint1  35334  bj-1nel0  35835  bj-sngltag  35864  bj-projval  35877  bj-elsn0  36036  bj-fununsn1  36134  tan2h  36480  lindsenlbs  36483  matunitlindf  36486  ptrest  36487  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem28  36516  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  prdsbnd  36661  rrnequiv  36703  grpokerinj  36761  rngoueqz  36808  gidsn  36820  0rngo  36895  isdmn3  36942  dibelval2nd  40023  hdmaprnlem9N  40728  hdmap14lem4a  40742  dvrelog2b  40931  sticksstones11  40972  0prjspnrel  41369  hbtlem5  41870  flcidc  41916  safesnsupfiss  42166  frege133d  42516  radcnvrat  43073  unisnALT  43687  sumsnd  43710  fnchoice  43713  rnsnf  43881  founiiun0  43888  elmapsnd  43903  fsneqrn  43910  infxrpnf  44156  supminfxr2  44179  cncfiooicc  44610  fperdvper  44635  dvmptfprodlem  44660  dvnprodlem1  44662  dvnprodlem2  44663  itgcoscmulx  44685  stoweidlem44  44760  fourierdlem49  44871  fourierdlem56  44878  fourierdlem80  44902  fourierdlem93  44915  fourierdlem101  44923  sge00  45092  sge0sn  45095  sge0snmpt  45099  sge0iunmptlemfi  45129  sge0p1  45130  sge0fodjrnlem  45132  sge0snmptf  45153  sge0splitsn  45157  nnfoctbdjlem  45171  meadjiunlem  45181  ismeannd  45183  caratheodorylem1  45242  isomenndlem  45246  hoidmv1le  45310  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem1  45317  hoiqssbl  45341  ovnovollem1  45372  ovnovollem2  45373  eldmressn  45747  iccpartltu  46093  sbgoldbo  46455  nnsum3primesprm  46458  bgoldbtbndlem3  46475  c0snmgmhm  46713  pzriprnglem12  46816  zrinitorngc  46898  ldepspr  47154  lmod1zr  47174