Theorem weq 1517

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

(Instead of introducing weq 1517 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 1364. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1517 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1364. 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 1364	1 wff x = y

Syntax hints:   = wceq 1364

This theorem is referenced by:  alequcoms  1530  equidqe  1546  ax4sp1  1547  spimfv  1713  chvarfv  1714  equid  1715  nfequid  1716  stdpc6  1717  equcomi  1718  ax6evr  1719  equcom  1720  equcomd  1721  equcoms  1722  equtr  1723  equtrr  1724  equtr2  1725  equequ1  1726  equequ2  1727  ax11i  1728  ax10o  1729  ax10  1731  nfae  1733  hbaes  1734  hbnae  1735  nfnae  1736  hbnaes  1737  equsalh  1740  equsal  1741  dral1  1744  dral2  1745  drex2  1746  drnf1  1747  drnf2  1748  spimth  1749  spimh  1751  spimed  1754  cbv1  1759  cbv1h  1760  cbv1v  1761  cbv2h  1762  cbv2w  1764  cbvalv1  1765  cbvexv1  1766  cbvalh  1767  chvar  1771  sbimi  1778  sb1  1780  sb2  1781  sbequ1  1782  sbequ2  1783  sbequ12  1785  sbequ12r  1786  sbequ12a  1787  sbid  1788  stdpc4  1789  sbh  1790  sb6x  1793  sbequ5  1796  sbequ6  1797  equsb1  1799  equsb2  1800  sbiedh  1801  sbiedv  1803  sbieh  1804  equsalv  1807  equs5a  1808  drsb1  1813  exdistrfor  1814  sb4a  1815  equs45f  1816  sb6f  1817  sb5f  1818  sb4e  1819  hbsb2a  1820  hbsb2e  1821  sbcof2  1824  aev  1826  ax16  1827  dveeq2  1829  dveeq2or  1830  ax11v2  1834  ax11a2  1835  ax11b  1840  equs5  1843  equs5or  1844  sb3  1845  sb4  1846  sb4or  1847  sb4b  1848  sb4bor  1849  hbsb2  1850  nfsb2or  1851  sbequi  1853  sbequ  1854  drsb2  1855  spsbe  1856  spsbim  1857  sbequ8  1861  sbidm  1865  sb5rf  1866  sb6rf  1867  ax16i  1872  spv  1874  speiv  1876  equvin  1877  a16g  1878  a16gb  1879  a16nf  1880  sb56  1900  sb6  1901  sb5  1902  sbnv  1903  sbanv  1904  sborv  1905  sbi1v  1906  sbi2v  1907  cbvalvw  1934  cbvexvw  1935  cbval2  1936  cbvex2  1937  cbvaldva  1943  cbvexdva  1944  cbvaldvaw  1945  cbval2vw  1947  cbvex2vw  1948  cbvex4v  1949  hbs1  1957  hbsbv  1960  nfsbxy  1961  nfsbxyt  1962  nfsbv  1966  equsb3  1970  sbco  1987  sbcocom  1989  sbcomxyyz  1991  sb9v  1997  2sb5  2002  2sb6  2003  sbcom2v  2004  sb6a  2007  2sb5rf  2008  2sb6rf  2009  dfsb7  2010  sb7f  2011  sb7af  2012  sb10f  2014  sbel2x  2017  sbalyz  2018  sbal1yz  2020  sbal1  2021  sbexyz  2022  exsb  2027  2exsb  2028  dvelimALT  2029  dvelimfv  2030  hbsb4t  2032  nfsb4t  2033  dvelimf  2034  dvelimdf  2035  dvelimor  2037  dveeq1  2038  sbal2  2039  euf  2050  eubidh  2051  eubid  2052  hbeu1  2055  nfeu1  2056  sb8eu  2058  nfeuv  2063  sb8euh  2068  eu1  2070  mo2n  2073  euex  2075  eumo0  2076  mo23  2086  mor  2087  modc  2088  eu2  2089  eu3h  2090  mo2r  2097  mo3h  2098  mo2dc  2100  mo4f  2105  eu4  2107  moim  2109  moimv  2111  moanim  2119  mopick  2123  2eu4  2138  euequ1  2140  exists1  2141  elequ1  2171  elequ2  2172  cleljust  2173  elsb1  2174  elsb2  2175  axext3  2179  axext4  2180  bm1.1  2181  eleq1w  2257  cleqh  2296  cbvabw  2319  cbvab  2320  sbab  2324  nfcjust  2327  drnfc1  2356  drnfc2  2357  nfabdw  2358  dvelimdc  2360  dvelimc  2361  nfcvf  2362  cbvralfw  2719  cbvrexfw  2720  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvralvw  2733  cbvrexvw  2734  cbvreuvw  2735  cbvraldva2  2736  cbvrexdva2  2737  cbvraldva  2738  cbvrexdva  2739  cbvral2vw  2740  cbvrex2vw  2741  cbvral2v  2742  cbvrex2v  2743  cbvral3v  2744  sbralie  2747  cbvrab  2761  vjust  2764  vex  2766  rr19.3v  2903  rr19.28v  2904  ralab2  2928  rexab2  2930  reu2  2952  reu6  2953  reu3  2954  rmo4  2957  reu4  2958  reu7  2959  reu8  2960  rmo3f  2961  rmo4f  2962  cdeqi  2974  cdeqri  2975  cdeqth  2976  cdeqnot  2977  cdeqal  2978  cdeqab  2979  cdeqim  2982  cdeqcv  2983  cdeqeq  2984  cdeqel  2985  nfccdeq  2987  sbsbc  2993  sbc8g  2997  sbcco2  3012  sbc5  3013  sbcralt  3066  sbcralg  3068  sbcreug  3070  rmo3  3081  cbvcsbw  3088  cbvcsb  3089  csbcow  3095  sbcel12g  3099  sbceqg  3100  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  difjust  3158  unjust  3160  injust  3162  dfss2f  3175  dfdif3  3274  dfnul3  3454  dfif3  3575  preq12bg  3804  eluniab  3852  elintab  3886  int0  3889  dfiunv2  3953  cbviun  3954  cbviin  3955  cbvdisj  4021  disjiun  4029  sndisj  4030  sbcbrg  4088  cbvmptf  4128  cbvmpt  4129  axsep2  4153  bm1.3ii  4155  nalset  4164  zfpow  4209  el  4212  dtruarb  4225  copsexg  4278  opelopabsb  4295  swopo  4342  pofun  4348  issod  4355  frind  4388  zfun  4470  ruv  4587  dtru  4597  dcextest  4618  tfisi  4624  findes  4640  relop  4817  dfdmf  4860  dfrnf  4908  resiexg  4992  dfres2  4999  opabresid  5000  mptresid  5001  imai  5026  issref  5053  intasym  5055  cnvi  5075  rnxpid  5105  cnvpom  5213  nfiota1  5222  cbviota  5225  sb8iota  5227  iotaval  5231  iotanul  5235  iota4  5239  eliota  5247  eliotaeu  5248  csbiotag  5252  dffun2  5269  dffun4  5270  dffun5r  5271  dffun6f  5272  dffun4f  5275  sbcfung  5283  funopg  5293  funinsn  5308  funcnveq  5322  fun11  5326  fununi  5327  funcnvuni  5328  imain  5341  isarep2  5346  brprcneu  5552  fv2  5554  elfv  5557  fv3  5582  relelfvdm  5591  fvmpt2  5646  ralrnmpt  5705  rexrnmpt  5706  ffnfvf  5722  f1veqaeq  5817  dff13f  5818  fliftfuns  5846  canth  5876  cbvriota  5889  csbriotag  5891  acexmid  5922  oprabidlem  5954  cbvmpox  6001  cbvmpo  6002  cbvmpov  6003  mpofun  6025  abrexex2  6182  fmpoco  6275  f1o2ndf1  6287  poxp  6291  tposoprab  6339  tfrlem3-2d  6371  tfrlemi1  6391  tfr1onlemsucfn  6399  tfr1onlemaccex  6407  tfrcllemsucfn  6412  tfrcllemsucaccv  6413  tfrcllembxssdm  6415  tfrcllembfn  6416  tfrcllemaccex  6420  dcdifsnid  6563  fnsnsplitdc  6564  funresdfunsndc  6565  eqerlem  6624  qliftfuns  6679  eroveu  6686  cbvixp  6775  mptelixpg  6794  idssen  6837  pw2f1odclem  6896  xpf1o  6906  xpmapen  6912  findcard2d  6953  nnwetri  6978  fiintim  6993  snexxph  7017  fidcenumlemim  7019  fidcenumlemrk  7021  fidcenum  7023  supmoti  7060  isoti  7074  supisoti  7077  cnvti  7086  ordiso2  7102  ctssdccl  7178  finct  7183  infnninf  7191  nninfwlpoim  7245  nninfwlpo  7246  exmidontriimlem3  7292  exmidontriimlem4  7293  exmidontriim  7294  onntri13  7307  onntri51  7309  onntri3or  7314  dftap2  7320  netap  7323  2onetap  7324  2omotaplemap  7326  cc1  7334  cc2  7336  ltsopi  7389  addpipqqs  7439  mulpipqqs  7442  archpr  7712  cauappcvgprlemlol  7716  cauappcvgprlemopu  7717  cauappcvgprlemupu  7718  cauappcvgprlemdisj  7720  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  cauappcvgprlemlim  7730  caucvgprlemlol  7739  caucvgprlemopu  7740  caucvgprlemupu  7741  caucvgprlemdisj  7743  caucvgprlemloc  7744  caucvgprlemcl  7745  caucvgprlemladdrl  7747  caucvgprprlemcbv  7756  caucvgprprlemopu  7768  caucvgprprlemclphr  7774  caucvgprprlemexbt  7775  suplocexprlemmu  7787  suplocexprlemdisj  7789  caucvgsrlembound  7863  caucvgsrlembnd  7870  suplocsrlem  7877  suplocsr  7878  peano1nnnn  7921  axcaucvglemres  7968  axpre-suploc  7971  negf1o  8410  lbreu  8974  lbinf  8977  suprubex  8980  suprlubex  8981  suprleubex  8983  1nn  9003  uzind4s  9666  uzind4s2  9667  indstr  9669  supinfneg  9671  infsupneg  9672  infregelbex  9674  eqreznegel  9690  lbzbi  9692  elpq  9725  zsupcl  10323  infssuzex  10325  infssuzledc  10326  zsupssdc  10330  exbtwnzlemex  10341  exbtwnz  10342  rebtwn2zlemstep  10344  rebtwn2z  10346  iseqovex  10552  iseqvalcbv  10553  seqvalcd  10555  seqovcd  10561  seq3f1olemqsum  10607  seq3f1olemp  10609  seq3f1oleml  10610  seqf1og  10615  seq3distr  10626  faclbnd6  10838  fimaxq  10921  cvg1nlemres  11152  resqrexlemsqa  11191  resqrexlemex  11192  cau3lem  11281  fclim  11461  climeu  11463  cn1lem  11481  climcau  11514  climcvg1n  11517  summodclem3  11547  summodclem2a  11548  summodclem2  11549  summodc  11550  zsumdc  11551  fsum3  11554  isumz  11556  isumss2  11560  fsumsersdc  11562  fsum3ser  11564  fsumadd  11573  fsum2dlemstep  11601  fisumcom2  11605  isumshft  11657  cvgratz  11699  mertensabs  11704  prodfdivap  11714  cbvprod  11725  prodmodclem3  11742  prodmodclem2a  11743  prodmodclem2  11744  prodmodc  11745  zproddc  11746  fprodseq  11750  fprodm1s  11768  fprodp1s  11769  fprod2dlemstep  11789  fprodcom2fi  11793  fprodsplitf  11799  odd2np1lem  12039  bitsfzolem  12121  bezoutlemmain  12175  bezoutlemeu  12184  gcdmultiple  12197  rplpwr  12204  nnwofdc  12215  nnwosdc  12216  nninfctlemfo  12217  isprm5lem  12319  isprm5  12320  pw2dvdseu  12346  hashdvds  12399  eulerthlemh  12409  reumodprminv  12432  pclemub  12466  pclemdc  12467  pceu  12474  pcmptdvds  12524  1arith  12546  4sqlem2  12568  4sqlem11  12580  4sqlem12  12581  ennnfonelemg  12630  ennnfoneleminc  12638  ennnfonelemkh  12639  ennnfonelemhf1o  12640  ennnfonelemex  12641  ennnfonelemhom  12642  ennnfonelemrnh  12643  ennnfonelemfun  12644  ennnfonelemdm  12647  ennnfonelemr  12650  ennnfone  12652  inffinp1  12656  ctinf  12657  nninfdclemf  12676  nninfdclemp1  12677  unbendc  12681  infpn2  12683  strsetsid  12721  mgmidmo  13025  lidrididd  13035  mndinvmod  13096  insubm  13127  dfgrp3mlem  13240  mulgaddcom  13286  mulginvcom  13287  isnsg2  13343  gsumfzconstf  13482  srgmulgass  13555  islmodd  13859  lmodvsmmulgdi  13889  rmodislmodlem  13916  rmodislmod  13917  lssats2  13980  baspartn  14296  cnpnei  14465  txdis1cn  14524  cnmptid  14527  xmetxp  14753  cncfmptc  14842  cncfmptid  14843  dedekindeulemloc  14865  dedekindicclemloc  14874  ivthinclemlr  14883  ivthinclemur  14885  ivthinclemloc  14887  ivthdec  14890  dvmptfsum  14971  plymullem1  14994  perfectlem2  15246  lgseisenlem2  15322  lgsquadlem3  15330  lgsquad  15331  lgsquad2lem2  15333  2lgslem1a  15339  spimd  15421  2spim  15422  ch2var  15423  bj-sbimedh  15427  bj-sbimeh  15428  cbvrald  15444  sumdc2  15455  bdth  15487  bdcdeq  15495  bdne  15509  bdreu  15511  bdcsn  15526  bdsep2  15542  bdsepnft  15543  bdsepnfALT  15545  bdbm1.3ii  15547  bj-nalset  15551  bj-zfpair2  15566  bj-bdfindes  15605  bj-nn0suc0  15606  bj-nntrans  15607  setindft  15621  setindis  15623  bdsetindis  15625  bj-inf2vnlem3  15628  bj-inf2vnlem4  15629  strcoll2  15639  strcollnft  15640  strcollnfALT  15642  sscoll2  15644  nnti  15649  nnsf  15659  peano4nninf  15660  nninfsellemqall  15669  nninfomni  15673  nnnninfen  15675  trilpolemeq1  15694  tridceq  15710  redc0  15711  reap0  15712  dceqnconst  15714  dcapnconst  15715  nconstwlpolemgt0  15718