Theorem elsni 4650

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  {csn 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-sn 4634

This theorem is referenced by:  elsn2g  4671  nelsn  4673  elpwunsn  4692  eqoreldif  4693  disjsn2  4721  rabsnifsb  4731  sssn  4835  disjxsn  5146  opth1  5481  sosn  5768  ressn  6296  elsnxp  6302  elsuci  6443  funcnvsn  6609  funopdmsn  7164  fvconst  7178  fnsnr  7179  fmptap  7184  mposnif  7541  1stconst  8114  2ndconst  8115  reldmtpos  8249  tpostpos  8261  disjen  9172  map2xp  9185  en1eqsn  9308  ac6sfi  9321  ixpfi2  9394  elfi2  9457  fisn  9470  unxpwdom2  9631  cantnfp1lem3  9723  djulf1o  9955  djurf1o  9956  djur  9962  eldju2ndl  9967  eldju2ndr  9968  isfin4p1  10358  dcomex  10490  iundom2g  10583  fpwwe2lem12  10685  canthp1lem2  10696  0tsk  10798  elreal2  11175  ax1rid  11204  ltxrlt  11334  un0addcl  12557  un0mulcl  12558  fzodisjsn  13724  elfzonlteqm1  13762  elfzo0l  13776  elfzr  13800  elfzlmr  13801  seqf1o  14063  seqid3  14066  seqz  14070  1exp  14111  hashnn0pnf  14359  hash1elsn  14388  hashprg  14412  cats1un  14729  fsumss  15729  sumsnf  15747  fsumsplitsn  15748  fsum2dlem  15774  fsumcom2  15778  ackbijnn  15832  fprodss  15950  fprod2dlem  15982  fprodcom2  15986  fprodsplitsn  15991  sumeven  16389  sumodd  16390  divalgmod  16408  lcmfunsnlem2lem1  16639  lcmfunsnlem2lem2  16640  phi1  16775  dfphi2  16776  nnnn0modprm0  16808  ramubcl  17020  0ram  17022  ramz  17027  imasvscafn  17552  mreexmrid  17656  2initoinv  18032  2termoinv  18039  gsumress  18675  gsumval2  18679  smndex1basss  18895  smndex1mndlem  18899  0nsg  19163  symgextf1lem  19418  symgextf1  19419  pmtrprfval  19485  psgnsn  19518  lsmdisj2  19680  subgdisj1  19689  lt6abl  19893  gsumsnfd  19949  gsumzunsnd  19954  gsumunsnfd  19955  gsum2dlem2  19969  dprdfeq0  20022  dprdsn  20036  dprd2da  20042  pgpfac1lem3a  20076  pgpfaclem2  20082  ablsimpnosubgd  20104  c0snmgmhm  20444  0ring01eq  20511  zrinitorngc  20620  lsssn0  20925  lspsneq0  20989  lspdisjb  21107  pzriprnglem12  21482  frgpcyg  21571  obselocv  21726  obs2ss  21727  mplcoe5  22047  psdmul  22160  coe1tm  22264  mat0dim0  22460  mat0dimid  22461  mat0dimscm  22462  mat1dimscm  22468  mavmul0g  22546  mdet0pr  22585  mdetunilem9  22613  cramer0  22683  pmatcollpw3fi1lem1  22779  basdif0  22947  ordtbas  23187  ordtrest2  23199  cmpfi  23403  refun0  23510  txdis1cn  23630  ptrescn  23634  txkgen  23647  xkoptsub  23649  ordthmeolem  23796  pt1hmeo  23801  filconn  23878  filufint  23915  flimclslem  23979  ptcmplem3  24049  idnghm  24751  iccpnfcnv  24960  iccpnfhmeo  24961  bndth  24975  ivthicc  25478  ovoliunlem1  25522  i1fima2sn  25700  i1f1  25710  itg1addlem4  25719  itg1addlem4OLD  25720  itg1addlem5  25721  i1fmulc  25724  limcres  25906  limccnp  25911  limccnp2  25912  degltlem1  26099  ply1rem  26193  fta1blem  26198  ig1pdvds  26207  plyeq0lem  26237  plypf1  26239  plyaddlem1  26240  plymullem1  26241  coemulhi  26281  plycj  26305  taylfval  26386  abelthlem3  26463  rlimcnp  26993  wilthlem2  27097  logexprlim  27254  2sqreultblem  27477  tgldim0eq  28430  edglnl  29079  nbgr1vtx  29294  vtxdginducedm1lem4  29479  clwlkclwwlklem2a4  29930  eucrct2eupth  30178  frgrncvvdeqlem9  30240  nsnlplig  30414  nsnlpligALT  30415  fsumiunle  32730  cshw1s2  32824  gsumhashmul  32925  xrge0tsmsbi  32927  cyc3evpm  33028  0ringcring  33107  pidlnz  33251  elrspunidl  33303  0ringprmidl  33324  drngmxidlr  33353  ig1pmindeg  33469  lbslsat  33511  lindsunlem  33519  irngnminplynz  33581  ordtrest2NEW  33738  xrge0iifcnv  33748  xrge0iifhom  33752  esumsnf  33897  esumpr  33899  esumiun  33927  inelpisys  33987  measvunilem0  34046  measvuni  34047  carsggect  34152  omsmeas  34157  plymulx0  34393  repr0  34457  bnj98  34712  bnj1442  34894  bnj1452  34897  subfacp1lem5  35012  erdszelem4  35022  erdszelem8  35026  sconnpi1  35067  cvmlift2lem6  35136  cvmlift2lem12  35142  fmla0xp  35211  onint1  36161  bj-1nel0  36661  bj-sngltag  36690  bj-projval  36703  bj-elsn0  36862  bj-fununsn1  36960  tan2h  37313  lindsenlbs  37316  matunitlindf  37319  ptrest  37320  poimirlem23  37344  poimirlem24  37345  poimirlem25  37346  poimirlem28  37349  poimirlem29  37350  poimirlem30  37351  poimirlem31  37352  poimirlem32  37353  prdsbnd  37494  rrnequiv  37536  grpokerinj  37594  rngoueqz  37641  gidsn  37653  0rngo  37728  isdmn3  37775  dibelval2nd  40851  hdmaprnlem9N  41556  hdmap14lem4a  41570  dvrelog2b  41765  sticksstones11  41854  0prjspnrel  42281  hbtlem5  42789  flcidc  42835  safesnsupfiss  43082  frege133d  43432  radcnvrat  43988  unisnALT  44602  sumsnd  44625  fnchoice  44628  rnsnf  44791  founiiun0  44797  elmapsnd  44811  fsneqrn  44818  infxrpnf  45061  supminfxr2  45084  cncfiooicc  45515  fperdvper  45540  dvmptfprodlem  45565  dvnprodlem1  45567  dvnprodlem2  45568  itgcoscmulx  45590  stoweidlem44  45665  fourierdlem49  45776  fourierdlem56  45783  fourierdlem80  45807  fourierdlem93  45820  fourierdlem101  45828  sge00  45997  sge0sn  46000  sge0snmpt  46004  sge0iunmptlemfi  46034  sge0p1  46035  sge0fodjrnlem  46037  sge0snmptf  46058  sge0splitsn  46062  nnfoctbdjlem  46076  meadjiunlem  46086  ismeannd  46088  caratheodorylem1  46147  isomenndlem  46151  hoidmv1le  46215  hoidmvlelem2  46217  hoidmvlelem3  46218  ovnhoilem1  46222  hoiqssbl  46246  ovnovollem1  46277  ovnovollem2  46278  eldmressn  46652  iccpartltu  46997  sbgoldbo  47359  nnsum3primesprm  47362  bgoldbtbndlem3  47379  ldepspr  47856  lmod1zr  47876