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

Theorem velsn 4556
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
velsn (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Proof of Theorem velsn
StepHypRef Expression
1 vex 3474 . 2 𝑥 ∈ V
21elsn 4555 1 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2115  {csn 4540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-sn 4541
This theorem is referenced by:  dfpr2  4559  ralsnsg  4581  rexsns  4582  disjsn  4620  snprc  4626  snssg  4690  raldifsnb  4702  difprsnss  4705  pwpw0  4719  eqsn  4735  snsspw  4748  pwsnOLD  4804  dfnfc2  4833  uni0b  4837  uni0c  4838  sndisj  5030  rext  5314  moabex  5324  exss  5328  otiunsndisj  5383  fconstmpt  5587  opeliunxp  5592  rnep  5770  restidsing  5895  xpdifid  5998  dmsnopg  6043  sniota  6319  dfmpt3  6455  nfunsn  6680  dffv2  6729  fsn  6870  fnasrn  6880  fnsnb  6901  fmptsng  6903  fmptsnd  6904  fvclss  6975  eusvobj2  7123  suceloni  7503  opabex3d  7641  opabex3rd  7642  opabex3  7643  wfrlem14  7943  wfrlem15  7944  oarec  8163  mapdm0  8396  ixp0x  8465  snmapen  8565  xpsnen  8576  marypha2lem2  8876  elirrv  9036  cantnfp1lem1  9117  cantnfp1lem3  9119  djuunxp  9326  dfac5lem1  9526  dfac5lem2  9527  dfac5lem4  9529  fin1a2lem11  9809  axdc4lem  9854  axcclem  9856  ttukeylem7  9914  xrsupexmnf  12676  xrinfmexpnf  12677  iccid  12761  fzsn  12932  fzpr  12945  seqz  13402  hashf1  13799  pr2pwpr  13821  s3iunsndisj  14307  fsum2dlem  15104  incexc2  15172  prodsn  15295  prodsnf  15297  fprod2dlem  15313  ef0lem  15411  lcmfunsnlem2  15961  1nprm  16000  vdwapun  16287  prmodvdslcmf  16360  cshwsiun  16412  mgmidsssn0  17861  mnd1id  17932  0subm  17961  efmnd1bas  18037  smndex1basss  18049  smndex1mgm  18051  trivsubgsnd  18285  symg1bas  18498  pmtrprfvalrn  18595  gex1  18695  sylow2alem1  18721  lsmdisj2  18787  0frgp  18884  0cyg  18992  prmcyg  18993  dprddisj2  19140  ablfacrp  19167  kerf1ghm  19474  lspdisj  19873  lidlnz  19977  psrlidm  20159  mplcoe1  20222  mplcoe5  20225  mulgrhm2  20622  ocvin  20794  maducoeval2  21225  madugsum  21228  en2top  21569  restsn  21754  ist1-3  21933  ordtt1  21963  cmpcld  21986  unisngl  22111  dissnlocfin  22113  ptopn2  22168  snfil  22448  alexsubALTlem2  22632  alexsubALTlem3  22633  alexsubALTlem4  22634  haustsms2  22721  tsmsxplem1  22737  tsmsxplem2  22738  ust0  22804  dscopn  23159  nmoid  23327  limcdif  24458  ellimc2  24459  limcmpt  24465  limcres  24468  ply1remlem  24742  plyeq0lem  24786  plyremlem  24879  aaliou2  24915  radcnv0  24990  abelthlem2  25006  wilthlem2  25633  vmappw  25680  ppinprm  25716  chtnprm  25718  musumsum  25756  dchrhash  25834  lgsquadlem1  25943  lgsquadlem2  25944  cplgr1v  27199  rusgrnumwwlkb0  27736  frgrncvvdeq  28073  fusgr2wsp2nb  28098  hsn0elch  29010  eqsnd  30276  cycpmrn  30793  qsxpid  30935  ccfldextdgrr  31068  xrge0iifiso  31186  qqhval2  31231  esumnul  31315  esumrnmpt2  31335  esumfzf  31336  sibfof  31606  sitgaddlemb  31614  plymulx0  31825  signstf0  31846  prodfzo03  31882  circlemeth  31919  bnj521  32015  sconnpi1  32494  dffr5  32997  eqfunresadj  33012  elima4  33027  frrlem12  33142  frrlem13  33143  brsingle  33386  dfiota3  33392  funpartfun  33412  dfrdg4  33420  fwddifn0  33633  bj-csbsnlem  34238  bj-pw0ALT  34360  bj-restsn  34391  bj-rest10  34397  mptsnunlem  34639  fvineqsneu  34712  matunitlindflem1  34935  poimirlem23  34962  poimirlem26  34965  poimirlem27  34966  grposnOLD  35202  0idl  35345  smprngopr  35372  isdmn3  35394  lshpdisj  36165  lsat0cv  36211  snatpsubN  36928  dibelval3  38325  dib1dim  38343  dvh2dim  38623  mapd0  38843  hdmap14lem13  39058  iunsn  39244  fnsnbt  39246  prjspeclsp  39413  pellexlem5  39581  jm2.23  39744  flcidc  39925  snhesn  40295  snssiALTVD  41344  snssiALT  41345  fsneq  41651  iccintsng  41979  icoiccdif  41980  limcrecl  42090  lptioo2  42092  lptioo1  42093  limcresiooub  42103  limcresioolb  42104  cnrefiisplem  42290  icccncfext  42348  dvmptfprodlem  42405  dvnprodlem3  42409  dirkercncflem2  42565  fourierdlem40  42608  fourierdlem48  42615  fourierdlem51  42618  fourierdlem62  42629  fourierdlem66  42633  fourierdlem74  42641  fourierdlem75  42642  fourierdlem76  42643  fourierdlem78  42645  fourierdlem79  42646  fourierdlem93  42660  fourierdlem101  42668  fourierdlem103  42670  fourierdlem104  42671  fouriersw  42692  elaa2  42695  etransclem44  42739  rrxsnicc  42761  sge00  42834  absnsb  43438  funressnfv  43454  dfdfat2  43503  tz6.12-afv  43548  tz6.12-afv2  43615  otiunsndisjX  43654  iccpartgtl  43762  iccpartgt  43763  iccpartleu  43764  iccpartgel  43765  nnsum4primeseven  44137  nnsum4primesevenALTV  44138  bgoldbtbnd  44146  xpsnopab  44204  opeliun2xp  44553  aacllem  45136
  Copyright terms: Public domain W3C validator