MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsni Structured version   Visualization version   GIF version

Theorem elsni 4142
Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
elsni (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Proof of Theorem elsni
StepHypRef Expression
1 elsng 4139 . 2 (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
21ibi 255 1 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sn 4126
This theorem is referenced by:  elsn2g  4157  nelsn  4159  elpwunsn  4171  eqoreldif  4172  eqoreldifOLD  4173  disjsn2  4193  rabsnifsb  4201  sssn  4298  disjxsn  4576  opth1  4870  sosn  5111  ressn  5588  elsnxp  5594  elsuci  5708  funcnvsn  5850  fvconst  6336  fnsnb  6337  fmptap  6341  mpt2snif  6652  1stconst  7152  2ndconst  7153  reldmtpos  7247  tpostpos  7259  disjen  8002  map2xp  8015  ac6sfi  8089  ixpfi2  8147  elfi2  8203  fisn  8216  unxpwdom2  8376  cantnfp1lem3  8460  isfin4-3  9020  dcomex  9152  iundom2g  9241  fpwwe2lem13  9343  canthp1lem2  9354  0tsk  9456  elreal2  9832  ax1rid  9861  ltxrlt  9987  un0addcl  11203  un0mulcl  11204  fzodisjsn  12374  elfzonlteqm1  12410  seqf1o  12704  seqid3  12707  seqz  12711  1exp  12751  hashnn0pnf  12992  hashprg  13043  hashprgOLD  13044  cats1un  13327  fsumss  14303  sumsn  14319  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  ackbijnn  14399  fprodss  14517  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fprodsplitsn  14559  sumeven  14948  sumodd  14949  divalgmod  14967  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  phi1  15316  dfphi2  15317  nnnn0modprm0  15349  ramubcl  15560  0ram  15562  ramz  15567  imasvscafn  16020  xpsc0  16043  xpsc1  16044  xpsfrnel2  16048  mreexmrid  16126  2initoinv  16483  2termoinv  16490  gsumress  17099  gsumval2  17103  0nsg  17462  symgextf1lem  17663  symgextf1  17664  pmtrprfval  17730  psgnsn  17763  lsmdisj2  17918  subgdisj1  17927  lt6abl  18119  gsumsnfd  18174  gsumzunsnd  18178  gsumunsnfd  18179  gsum2dlem2  18193  dprdfeq0  18244  dprdsn  18258  dprd2da  18264  pgpfac1lem3a  18298  pgpfaclem2  18304  lsssn0  18769  lspsneq0  18833  lspdisjb  18947  0ring01eq  19092  mplcoe5  19289  coe1tm  19464  frgpcyg  19741  obselocv  19891  obs2ss  19892  mat0dim0  20092  mat0dimid  20093  mat0dimscm  20094  mat1dimscm  20100  mavmul0g  20178  mdet0pr  20217  mdetunilem9  20245  cramer0  20315  pmatcollpw3fi1lem1  20410  basdif0  20568  ordtbas  20806  ordtrest2  20818  cmpfi  21021  refun0  21128  txdis1cn  21248  ptrescn  21252  txkgen  21265  xkoptsub  21267  ordthmeolem  21414  pt1hmeo  21419  filcon  21497  filufint  21534  flimclslem  21598  ptcmplem3  21668  idnghm  22357  iccpnfcnv  22551  iccpnfhmeo  22552  bndth  22565  ivthicc  23034  ovoliunlem1  23077  i1fima2sn  23253  i1f1  23263  itg1addlem4  23272  itg1addlem5  23273  i1fmulc  23276  limcres  23456  limccnp  23461  limccnp2  23462  degltlem1  23636  ply1rem  23727  fta1blem  23732  ig1pdvds  23740  plyeq0lem  23770  plypf1  23772  plyaddlem1  23773  plymullem1  23774  coemulhi  23814  plycj  23837  taylfval  23917  abelthlem3  23991  rlimcnp  24492  wilthlem2  24595  logexprlim  24750  tgldim0eq  25198  nbcusgra  25992  uvtxnbgra  26021  clwlkisclwwlklem2a4  26312  vdgr1d  26430  vdgr1b  26431  vdgr1a  26433  eupap1  26503  frgraunss  26522  vdgfrgragt2  26554  frgrancvvdeqlemC  26566  frgrawopreglem2  26572  xrge0tsmsbi  29117  ordtrest2NEW  29297  xrge0iifcnv  29307  xrge0iifhom  29311  esumsnf  29453  esumpr  29455  esumiun  29483  inelpisys  29544  measvunilem0  29603  measvuni  29604  carsggect  29707  omsmeas  29712  plymulx0  29950  bnj142OLD  30048  bnj98  30191  bnj1442  30371  bnj1452  30374  subfacp1lem5  30420  erdszelem4  30430  erdszelem8  30434  sconpi1  30475  cvmlift2lem6  30544  cvmlift2lem12  30550  onint1  31618  bj-1nel0  32134  bj-sngltag  32164  bj-projval  32177  tan2h  32571  lindsenlbs  32574  matunitlindf  32577  ptrest  32578  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  prdsbnd  32762  rrnequiv  32804  grpokerinj  32862  rngoueqz  32909  gidsn  32921  0rngo  32996  isdmn3  33043  dibelval2nd  35459  hdmaprnlem9N  36167  hdmap14lem4a  36181  hbtlem5  36717  flcidc  36763  frege133d  37076  radcnvrat  37535  unisnALT  38184  sumsnd  38208  fnchoice  38211  rnsnf  38365  founiiun0  38372  elmapsnd  38391  fsneqrn  38398  sumsnf  38636  fsumsplitsn  38637  cncfiooicc  38780  fperdvper  38808  dvmptfprodlem  38834  dvnprodlem1  38836  dvnprodlem2  38837  itgcoscmulx  38861  stoweidlem44  38937  fourierdlem49  39048  fourierdlem56  39055  fourierdlem80  39079  fourierdlem93  39092  fourierdlem101  39100  sge00  39269  sge0sn  39272  sge0snmpt  39276  sge0iunmptlemfi  39306  sge0p1  39307  sge0fodjrnlem  39309  sge0snmptf  39330  sge0splitsn  39334  nnfoctbdjlem  39348  meadjiunlem  39358  ismeannd  39360  caratheodorylem1  39416  isomenndlem  39420  hoidmv1le  39484  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem1  39491  hoiqssbl  39515  ovnovollem1  39546  ovnovollem2  39547  eldmressn  39852  iccpartltu  39963  nnsum3primesprm  40206  bgoldbtbndlem3  40223  elfzr  40364  elfzo0l  40365  elfzlmr  40366  nbgr1vtx  40580  clwlkclwwlklem2a4  41206  eucrct2eupth  41413  frgrncvvdeqlemC  41478  c0snmgmhm  41704  zrinitorngc  41792  ldepspr  42056  lmod1zr  42076
  Copyright terms: Public domain W3C validator