Theorem weq 1513

Description: Extend wff definition to include atomic formulas using the equality predicate.

(Instead of introducing weq 1513 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wceq 1363. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1513 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1363. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.) (Contributed by NM, 24-Jan-2006.)

Assertion

Ref	Expression
weq	wff x = y

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1363	1 wff x = y

Syntax hints:   = wceq 1363

This theorem is referenced by:  alequcoms  1526  equidqe  1542  ax4sp1  1543  spimfv  1709  chvarfv  1710  equid  1711  nfequid  1712  stdpc6  1713  equcomi  1714  ax6evr  1715  equcom  1716  equcomd  1717  equcoms  1718  equtr  1719  equtrr  1720  equtr2  1721  equequ1  1722  equequ2  1723  ax11i  1724  ax10o  1725  ax10  1727  nfae  1729  hbaes  1730  hbnae  1731  nfnae  1732  hbnaes  1733  equsalh  1736  equsal  1737  dral1  1740  dral2  1741  drex2  1742  drnf1  1743  drnf2  1744  spimth  1745  spimh  1747  spimed  1750  cbv1  1755  cbv1h  1756  cbv1v  1757  cbv2h  1758  cbv2w  1760  cbvalv1  1761  cbvexv1  1762  cbvalh  1763  chvar  1767  sbimi  1774  sb1  1776  sb2  1777  sbequ1  1778  sbequ2  1779  sbequ12  1781  sbequ12r  1782  sbequ12a  1783  sbid  1784  stdpc4  1785  sbh  1786  sb6x  1789  sbequ5  1792  sbequ6  1793  equsb1  1795  equsb2  1796  sbiedh  1797  sbiedv  1799  sbieh  1800  equsalv  1803  equs5a  1804  drsb1  1809  exdistrfor  1810  sb4a  1811  equs45f  1812  sb6f  1813  sb5f  1814  sb4e  1815  hbsb2a  1816  hbsb2e  1817  sbcof2  1820  aev  1822  ax16  1823  dveeq2  1825  dveeq2or  1826  ax11v2  1830  ax11a2  1831  ax11b  1836  equs5  1839  equs5or  1840  sb3  1841  sb4  1842  sb4or  1843  sb4b  1844  sb4bor  1845  hbsb2  1846  nfsb2or  1847  sbequi  1849  sbequ  1850  drsb2  1851  spsbe  1852  spsbim  1853  sbequ8  1857  sbidm  1861  sb5rf  1862  sb6rf  1863  ax16i  1868  spv  1870  speiv  1872  equvin  1873  a16g  1874  a16gb  1875  a16nf  1876  sb56  1895  sb6  1896  sb5  1897  sbnv  1898  sbanv  1899  sborv  1900  sbi1v  1901  sbi2v  1902  cbvalvw  1929  cbvexvw  1930  cbval2  1931  cbvex2  1932  cbvaldva  1938  cbvexdva  1939  cbvex4v  1940  hbs1  1948  hbsbv  1951  nfsbxy  1952  nfsbxyt  1953  nfsbv  1957  equsb3  1961  sbco  1978  sbcocom  1980  sbcomxyyz  1982  sb9v  1988  2sb5  1993  2sb6  1994  sbcom2v  1995  sb6a  1998  2sb5rf  1999  2sb6rf  2000  dfsb7  2001  sb7f  2002  sb7af  2003  sb10f  2005  sbel2x  2008  sbalyz  2009  sbal1yz  2011  sbal1  2012  sbexyz  2013  exsb  2018  2exsb  2019  dvelimALT  2020  dvelimfv  2021  hbsb4t  2023  nfsb4t  2024  dvelimf  2025  dvelimdf  2026  dvelimor  2028  dveeq1  2029  sbal2  2030  euf  2041  eubidh  2042  eubid  2043  hbeu1  2046  nfeu1  2047  sb8eu  2049  nfeuv  2054  sb8euh  2059  eu1  2061  mo2n  2064  euex  2066  eumo0  2067  mo23  2077  mor  2078  modc  2079  eu2  2080  eu3h  2081  mo2r  2088  mo3h  2089  mo2dc  2091  mo4f  2096  eu4  2098  moim  2100  moimv  2102  moanim  2110  mopick  2114  2eu4  2129  euequ1  2131  exists1  2132  elequ1  2162  elequ2  2163  cleljust  2164  elsb1  2165  elsb2  2166  axext3  2170  axext4  2171  bm1.1  2172  eleq1w  2248  cleqh  2287  cbvabw  2310  cbvab  2311  sbab  2315  nfcjust  2317  drnfc1  2346  drnfc2  2347  nfabdw  2348  dvelimdc  2350  dvelimc  2351  nfcvf  2352  cbvralfw  2705  cbvrexfw  2706  cbvralf  2707  cbvrexf  2708  cbvreu  2713  cbvralvw  2719  cbvrexvw  2720  cbvreuvw  2721  cbvraldva2  2722  cbvrexdva2  2723  cbvraldva  2724  cbvrexdva  2725  cbvral2vw  2726  cbvrex2vw  2727  cbvral2v  2728  cbvrex2v  2729  cbvral3v  2730  sbralie  2733  cbvrab  2747  vjust  2750  vex  2752  rr19.3v  2888  rr19.28v  2889  ralab2  2913  rexab2  2915  reu2  2937  reu6  2938  reu3  2939  rmo4  2942  reu4  2943  reu7  2944  reu8  2945  rmo3f  2946  rmo4f  2947  cdeqi  2959  cdeqri  2960  cdeqth  2961  cdeqnot  2962  cdeqal  2963  cdeqab  2964  cdeqim  2967  cdeqcv  2968  cdeqeq  2969  cdeqel  2970  nfccdeq  2972  sbsbc  2978  sbc8g  2982  sbcco2  2997  sbc5  2998  sbcralt  3051  sbcralg  3053  sbcreug  3055  rmo3  3066  cbvcsbw  3073  cbvcsb  3074  csbcow  3080  sbcel12g  3084  sbceqg  3085  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  difjust  3142  unjust  3144  injust  3146  dfss2f  3158  dfdif3  3257  dfnul3  3437  dfif3  3559  preq12bg  3785  eluniab  3833  elintab  3867  int0  3870  dfiunv2  3934  cbviun  3935  cbviin  3936  cbvdisj  4002  disjiun  4010  sndisj  4011  sbcbrg  4069  cbvmptf  4109  cbvmpt  4110  axsep2  4134  bm1.3ii  4136  nalset  4145  zfpow  4187  el  4190  dtruarb  4203  copsexg  4256  opelopabsb  4272  swopo  4318  pofun  4324  issod  4331  frind  4364  zfun  4446  ruv  4561  dtru  4571  dcextest  4592  tfisi  4598  findes  4614  relop  4789  dfdmf  4832  dfrnf  4880  resiexg  4964  dfres2  4971  opabresid  4972  mptresid  4973  imai  4996  issref  5023  intasym  5025  cnvi  5045  rnxpid  5075  cnvpom  5183  nfiota1  5192  cbviota  5195  sb8iota  5197  iotaval  5201  iotanul  5205  iota4  5208  eliota  5216  eliotaeu  5217  csbiotag  5221  dffun2  5238  dffun4  5239  dffun5r  5240  dffun6f  5241  dffun4f  5244  sbcfung  5252  funopg  5262  funinsn  5277  funcnveq  5291  fun11  5295  fununi  5296  funcnvuni  5297  imain  5310  isarep2  5315  brprcneu  5520  fv2  5522  elfv  5525  fv3  5550  relelfvdm  5559  fvmpt2  5612  ralrnmpt  5671  rexrnmpt  5672  ffnfvf  5688  f1veqaeq  5783  dff13f  5784  fliftfuns  5812  canth  5842  cbvriota  5854  csbriotag  5856  acexmid  5887  oprabidlem  5919  cbvmpox  5966  cbvmpo  5967  cbvmpov  5968  mpofun  5990  abrexex2  6138  fmpoco  6230  f1o2ndf1  6242  poxp  6246  tposoprab  6294  tfrlem3-2d  6326  tfrlemi1  6346  tfr1onlemsucfn  6354  tfr1onlemaccex  6362  tfrcllemsucfn  6367  tfrcllemsucaccv  6368  tfrcllembxssdm  6370  tfrcllembfn  6371  tfrcllemaccex  6375  dcdifsnid  6518  fnsnsplitdc  6519  funresdfunsndc  6520  eqerlem  6579  qliftfuns  6632  eroveu  6639  cbvixp  6728  mptelixpg  6747  idssen  6790  xpf1o  6857  xpmapen  6863  findcard2d  6904  nnwetri  6928  fiintim  6941  snexxph  6962  fidcenumlemim  6964  fidcenumlemrk  6966  fidcenum  6968  supmoti  7005  isoti  7019  supisoti  7022  cnvti  7031  ordiso2  7047  ctssdccl  7123  finct  7128  infnninf  7135  nninfwlpoim  7189  nninfwlpo  7190  exmidontriimlem3  7235  exmidontriimlem4  7236  exmidontriim  7237  onntri13  7250  onntri51  7252  onntri3or  7257  dftap2  7263  netap  7266  2onetap  7267  2omotaplemap  7269  cc1  7277  cc2  7279  ltsopi  7332  addpipqqs  7382  mulpipqqs  7385  archpr  7655  cauappcvgprlemlol  7659  cauappcvgprlemopu  7660  cauappcvgprlemupu  7661  cauappcvgprlemdisj  7663  cauappcvgprlemladdru  7668  cauappcvgprlemladdrl  7669  cauappcvgprlemlim  7673  caucvgprlemlol  7682  caucvgprlemopu  7683  caucvgprlemupu  7684  caucvgprlemdisj  7686  caucvgprlemloc  7687  caucvgprlemcl  7688  caucvgprlemladdrl  7690  caucvgprprlemcbv  7699  caucvgprprlemopu  7711  caucvgprprlemclphr  7717  caucvgprprlemexbt  7718  suplocexprlemmu  7730  suplocexprlemdisj  7732  caucvgsrlembound  7806  caucvgsrlembnd  7813  suplocsrlem  7820  suplocsr  7821  peano1nnnn  7864  axcaucvglemres  7911  axpre-suploc  7914  negf1o  8352  lbreu  8915  lbinf  8918  suprubex  8921  suprlubex  8922  suprleubex  8924  1nn  8943  uzind4s  9603  uzind4s2  9604  indstr  9606  supinfneg  9608  infsupneg  9609  infregelbex  9611  eqreznegel  9627  lbzbi  9629  elpq  9661  exbtwnzlemex  10263  exbtwnz  10264  rebtwn2zlemstep  10266  rebtwn2z  10268  iseqovex  10469  iseqvalcbv  10470  seqvalcd  10472  seqovcd  10476  seq3f1olemqsum  10513  seq3f1olemp  10515  seq3f1oleml  10516  seq3distr  10526  faclbnd6  10737  fimaxq  10820  cvg1nlemres  11007  resqrexlemsqa  11046  resqrexlemex  11047  cau3lem  11136  fclim  11315  climeu  11317  cn1lem  11335  climcau  11368  climcvg1n  11371  summodclem3  11401  summodclem2a  11402  summodclem2  11403  summodc  11404  zsumdc  11405  fsum3  11408  isumz  11410  isumss2  11414  fsumsersdc  11416  fsum3ser  11418  fsumadd  11427  fsum2dlemstep  11455  fisumcom2  11459  isumshft  11511  cvgratz  11553  mertensabs  11558  prodfdivap  11568  cbvprod  11579  prodmodclem3  11596  prodmodclem2a  11597  prodmodclem2  11598  prodmodc  11599  zproddc  11600  fprodseq  11604  fprodm1s  11622  fprodp1s  11623  fprod2dlemstep  11643  fprodcom2fi  11647  fprodsplitf  11653  odd2np1lem  11890  zsupcl  11961  infssuzex  11963  infssuzledc  11964  zsupssdc  11968  bezoutlemmain  12012  bezoutlemeu  12021  gcdmultiple  12034  rplpwr  12041  nnwofdc  12052  nnwosdc  12053  isprm5lem  12154  isprm5  12155  pw2dvdseu  12181  hashdvds  12234  eulerthlemh  12244  reumodprminv  12266  pclemub  12300  pclemdc  12301  pceu  12308  pcmptdvds  12356  1arith  12378  4sqlem2  12400  ennnfonelemg  12417  ennnfoneleminc  12425  ennnfonelemkh  12426  ennnfonelemhf1o  12427  ennnfonelemex  12428  ennnfonelemhom  12429  ennnfonelemrnh  12430  ennnfonelemfun  12431  ennnfonelemdm  12434  ennnfonelemr  12437  ennnfone  12439  inffinp1  12443  ctinf  12444  nninfdclemf  12463  nninfdclemp1  12464  unbendc  12468  infpn2  12470  strsetsid  12508  mgmidmo  12809  lidrididd  12819  mndinvmod  12867  insubm  12893  dfgrp3mlem  12994  mulgaddcom  13038  mulginvcom  13039  isnsg2  13094  srgmulgass  13236  islmodd  13477  lmodvsmmulgdi  13507  rmodislmodlem  13534  rmodislmod  13535  lssats2  13598  baspartn  13821  cnpnei  13990  txdis1cn  14049  cnmptid  14052  xmetxp  14278  cncfmptc  14353  cncfmptid  14354  dedekindeulemloc  14368  dedekindicclemloc  14377  ivthinclemlr  14386  ivthinclemur  14388  ivthinclemloc  14390  ivthdec  14393  lgseisenlem2  14722  spimd  14788  2spim  14789  ch2var  14790  bj-sbimedh  14794  bj-sbimeh  14795  cbvrald  14811  sumdc2  14822  bdth  14854  bdcdeq  14862  bdne  14876  bdreu  14878  bdcsn  14893  bdsep2  14909  bdsepnft  14910  bdsepnfALT  14912  bdbm1.3ii  14914  bj-nalset  14918  bj-zfpair2  14933  bj-bdfindes  14972  bj-nn0suc0  14973  bj-nntrans  14974  setindft  14988  setindis  14990  bdsetindis  14992  bj-inf2vnlem3  14995  bj-inf2vnlem4  14996  strcoll2  15006  strcollnft  15007  strcollnfALT  15009  sscoll2  15011  nnti  15016  nnsf  15026  peano4nninf  15027  nninfsellemqall  15036  nninfomni  15040  trilpolemeq1  15060  tridceq  15076  redc0  15077  reap0  15078  dceqnconst  15080  dcapnconst  15081  nconstwlpolemgt0  15084