Theorem elsni 4608

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-sn 4592

This theorem is used by:  elsnd  4609  elsn2g  4632  nelsn  4634  elpwunsn  4652  eqoreldif  4653  disjsn2  4680  rabsnifsb  4690  sssn  4794  disjxsn  5105  opth1  5459  sosn  5750  ressn  6290  elsnxp  6296  elsuci  6434  funcnvsn  6590  funopdmsn  7153  fvconst  7166  fnsnr  7167  fmptap  7174  mposnif  7535  resf1extb  7937  1stconst  8101  2ndconst  8102  reldmtpos  8236  tpostpos  8248  disjen  9129  map2xp  9142  en1eqsn  9242  ac6sfi  9251  ixpfi2  9314  elfi2  9381  fisn  9394  unxpwdom2  9557  cantnfp1lem3  9656  djulf1o  9914  djurf1o  9915  djur  9921  eldju2ndl  9926  eldju2ndr  9927  isfin4p1  10314  dcomex  10446  iundom2g  10539  fpwwe2lem12  10642  canthp1lem2  10653  0tsk  10755  elreal2  11132  ax1rid  11161  ltxrlt  11295  un0addcl  12552  un0mulcl  12553  fzodisjsn  13743  elfzonlteqm1  13787  elfzo0l  13802  elfzr  13827  elfzlmr  13828  seqf1o  14097  seqid3  14100  seqz  14104  1exp  14145  hashnn0pnf  14396  hash1elsn  14425  hashprg  14449  cats1un  14780  fsumss  15799  sumsnf  15817  fsumsplitsn  15818  fsum2dlem  15844  fsumcom2  15848  ackbijnn  15905  fprodss  16025  fprod2dlem  16057  fprodcom2  16061  fprodsplitsn  16066  sumeven  16467  sumodd  16468  divalgmod  16486  lcmfunsnlem2lem1  16718  lcmfunsnlem2lem2  16719  phi1  16854  dfphi2  16855  nnnn0modprm0  16888  ramubcl  17100  0ram  17102  ramz  17107  imasvscafn  17613  mreexmrid  17721  2initoinv  18089  2termoinv  18096  gsumress  18772  gsumval2  18776  smndex1basss  19004  smndex1mndlem  19008  0nsg  19279  symgextf1lem  19534  symgextf1  19535  pmtrprfval  19601  psgnsn  19634  lsmdisj2  19796  subgdisj1  19805  lt6abl  20009  gsumsnfd  20065  gsumzunsnd  20070  gsumunsnfd  20071  gsum2dlem2  20085  dprdfeq0  20138  dprdsn  20152  dprd2da  20158  pgpfac1lem3a  20192  pgpfaclem2  20198  ablsimpnosubgd  20220  c0snmgmhm  20590  0ring01eq  20677  zrinitorngc  20791  lsssn0  21119  lspsneq0  21183  lspdisjb  21300  pidlnz  21424  0ringprmidl  21527  pzriprnglem12  21692  frgpcyg  21773  obselocv  21928  obs2ss  21929  mplcoe5  22241  psdmul  22379  coe1tm  22484  mat0dim0  22674  mat0dimid  22675  mat0dimscm  22676  mat1dimscm  22682  mavmul0g  22760  mdet0pr  22799  mdetunilem9  22827  cramer0  22897  pmatcollpw3fi1lem1  22993  basdif0  23160  ordtbas  23399  ordtrest2  23411  cmpfi  23615  refun0  23723  txdis1cn  23843  ptrescn  23847  txkgen  23860  xkoptsub  23862  ordthmeolem  24009  pt1hmeo  24014  filconn  24091  filufint  24128  flimclslem  24192  ptcmplem3  24262  idnghm  24951  iccpnfcnv  25154  iccpnfhmeo  25155  bndth  25168  ivthicc  25668  ovoliunlem1  25712  i1fima2sn  25890  i1f1  25900  itg1addlem4  25909  itg1addlem5  25910  i1fmulc  25913  limcres  26096  limccnp  26101  limccnp2  26102  degltlem1  26280  ply1rem  26374  fta1blem  26379  ig1pdvds  26388  plyeq0lem  26418  plypf1  26420  plyaddlem1  26421  plymullem1  26422  coemulhi  26462  plycj  26485  plycjOLD  26487  plyn0mulidp  26493  taylfval  26573  abelthlem3  26647  rlimcnp  27181  wilthlem2  27284  logexprlim  27440  2sqreultblem  27663  tgldim0eq  28823  edglnl  29548  nbgr1vtx  29766  vtxdginducedm1lem4  29950  clwlkclwwlklem2a4  30415  eucrct2eupth  30667  frgrncvvdeqlem9  30729  nsnlplig  30904  nsnlpligALT  30905  fsumiunle  33243  cshw1s2  33344  gsumhashmul  33451  xrge0tsmsbi  33458  gsumwrd2dccatlem  33461  cyc3evpm  33534  0ringcring  33636  elrspunidl  33800  drngmxidlr  33824  ig1pmindeg  33956  0mplrim  33968  selvply1rhmlemb  33973  mplmulmvr  33993  vieta  34034  lbslsat  34070  lindsunlem  34078  irngnminplynz  34166  ordtrest2NEW  34377  xrge0iifcnv  34387  xrge0iifhom  34391  esumsnf  34518  esumpr  34520  esumiun  34548  inelpisys  34609  measvunilem0  34668  measvuni  34669  carsggect  34773  omsmeas  34778  repr0  35063  bnj98  35320  bnj1442  35502  bnj1452  35505  subfacp1lem5  35713  erdszelem4  35723  erdszelem8  35727  sconnpi1  35768  cvmlift2lem6  35837  cvmlift2lem12  35843  fmla0xp  35912  onint1  37017  dfttc4lem2  37097  bj-1nel0  37647  bj-sngltag  37676  bj-projval  37689  bj-elsn0  37856  bj-fununsn1  37954  tan2h  38320  lindsenlbs  38323  matunitlindf  38326  ptrest  38327  poimirlem23  38351  poimirlem24  38352  poimirlem25  38353  poimirlem28  38356  poimirlem29  38357  poimirlem30  38358  poimirlem31  38359  poimirlem32  38360  prdsbnd  38502  rrnequiv  38544  grpokerinj  38602  rngoueqz  38649  gidsn  38661  0rngo  38736  isdmn3  38783  dibelval2nd  41984  hdmaprnlem9N  42689  hdmap14lem4a  42703  dvrelog2b  42891  sticksstones11  42981  unitscyglem2  43021  0prjspnrel  43417  hbtlem5  43913  flcidc  43955  safesnsupfiss  44199  frege133d  44549  radcnvrat  45082  unisnALT  45692  sumsnd  45804  fnchoice  45807  rnsnf  45960  founiiun0  45966  elmapsnd  45979  fsneqrn  45985  infxrpnf  46218  supminfxr2  46241  cncfiooicc  46666  fperdvper  46691  dvmptfprodlem  46716  dvnprodlem1  46718  dvnprodlem2  46719  itgcoscmulx  46741  stoweidlem44  46816  fourierdlem49  46927  fourierdlem56  46934  fourierdlem80  46958  fourierdlem93  46971  fourierdlem101  46979  sge00  47148  sge0sn  47151  sge0snmpt  47155  sge0iunmptlemfi  47185  sge0p1  47186  sge0fodjrnlem  47188  sge0snmptf  47209  sge0splitsn  47213  nnfoctbdjlem  47227  meadjiunlem  47237  ismeannd  47239  caratheodorylem1  47298  isomenndlem  47302  hoidmv1le  47366  hoidmvlelem2  47368  hoidmvlelem3  47369  ovnhoilem1  47373  hoiqssbl  47397  ovnovollem1  47428  ovnovollem2  47429  chnerlem1  47656  eldmressn  47832  iccpartltu  48232  sbgoldbo  48610  nnsum3primesprm  48613  bgoldbtbndlem3  48630  stgr1  48784  gpgprismgr4cycllem7  48924  isidom3  49167  ldepspr  49310  lmod1zr  49330  termcbas2  50317  idfudiag1  50360