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  3174  dfdif3  3273  dfnul3  3453  dfif3  3574  preq12bg  3803  eluniab  3851  elintab  3885  int0  3888  dfiunv2  3952  cbviun  3953  cbviin  3954  cbvdisj  4020  disjiun  4028  sndisj  4029  sbcbrg  4087  cbvmptf  4127  cbvmpt  4128  axsep2  4152  bm1.3ii  4154  nalset  4163  zfpow  4208  el  4211  dtruarb  4224  copsexg  4277  opelopabsb  4294  swopo  4341  pofun  4347  issod  4354  frind  4387  zfun  4469  ruv  4586  dtru  4596  dcextest  4617  tfisi  4623  findes  4639  relop  4816  dfdmf  4859  dfrnf  4907  resiexg  4991  dfres2  4998  opabresid  4999  mptresid  5000  imai  5025  issref  5052  intasym  5054  cnvi  5074  rnxpid  5104  cnvpom  5212  nfiota1  5221  cbviota  5224  sb8iota  5226  iotaval  5230  iotanul  5234  iota4  5238  eliota  5246  eliotaeu  5247  csbiotag  5251  dffun2  5268  dffun4  5269  dffun5r  5270  dffun6f  5271  dffun4f  5274  sbcfung  5282  funopg  5292  funinsn  5307  funcnveq  5321  fun11  5325  fununi  5326  funcnvuni  5327  imain  5340  isarep2  5345  brprcneu  5551  fv2  5553  elfv  5556  fv3  5581  relelfvdm  5590  fvmpt2  5645  ralrnmpt  5704  rexrnmpt  5705  ffnfvf  5721  f1veqaeq  5816  dff13f  5817  fliftfuns  5845  canth  5875  cbvriota  5888  csbriotag  5890  acexmid  5921  oprabidlem  5953  cbvmpox  6000  cbvmpo  6001  cbvmpov  6002  mpofun  6024  abrexex2  6181  fmpoco  6274  f1o2ndf1  6286  poxp  6290  tposoprab  6338  tfrlem3-2d  6370  tfrlemi1  6390  tfr1onlemsucfn  6398  tfr1onlemaccex  6406  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemaccex  6419  dcdifsnid  6562  fnsnsplitdc  6563  funresdfunsndc  6564  eqerlem  6623  qliftfuns  6678  eroveu  6685  cbvixp  6774  mptelixpg  6793  idssen  6836  pw2f1odclem  6895  xpf1o  6905  xpmapen  6911  findcard2d  6952  nnwetri  6977  fiintim  6992  snexxph  7016  fidcenumlemim  7018  fidcenumlemrk  7020  fidcenum  7022  supmoti  7059  isoti  7073  supisoti  7076  cnvti  7085  ordiso2  7101  ctssdccl  7177  finct  7182  infnninf  7190  nninfwlpoim  7244  nninfwlpo  7245  exmidontriimlem3  7290  exmidontriimlem4  7291  exmidontriim  7292  onntri13  7305  onntri51  7307  onntri3or  7312  dftap2  7318  netap  7321  2onetap  7322  2omotaplemap  7324  cc1  7332  cc2  7334  ltsopi  7387  addpipqqs  7437  mulpipqqs  7440  archpr  7710  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlemlim  7728  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdrl  7745  caucvgprprlemcbv  7754  caucvgprprlemopu  7766  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  suplocexprlemmu  7785  suplocexprlemdisj  7787  caucvgsrlembound  7861  caucvgsrlembnd  7868  suplocsrlem  7875  suplocsr  7876  peano1nnnn  7919  axcaucvglemres  7966  axpre-suploc  7969  negf1o  8408  lbreu  8972  lbinf  8975  suprubex  8978  suprlubex  8979  suprleubex  8981  1nn  9001  uzind4s  9664  uzind4s2  9665  indstr  9667  supinfneg  9669  infsupneg  9670  infregelbex  9672  eqreznegel  9688  lbzbi  9690  elpq  9723  zsupcl  10321  infssuzex  10323  infssuzledc  10324  zsupssdc  10328  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2z  10344  iseqovex  10550  iseqvalcbv  10551  seqvalcd  10553  seqovcd  10559  seq3f1olemqsum  10605  seq3f1olemp  10607  seq3f1oleml  10608  seqf1og  10613  seq3distr  10624  faclbnd6  10836  fimaxq  10919  cvg1nlemres  11150  resqrexlemsqa  11189  resqrexlemex  11190  cau3lem  11279  fclim  11459  climeu  11461  cn1lem  11479  climcau  11512  climcvg1n  11515  summodclem3  11545  summodclem2a  11546  summodclem2  11547  summodc  11548  zsumdc  11549  fsum3  11552  isumz  11554  isumss2  11558  fsumsersdc  11560  fsum3ser  11562  fsumadd  11571  fsum2dlemstep  11599  fisumcom2  11603  isumshft  11655  cvgratz  11697  mertensabs  11702  prodfdivap  11712  cbvprod  11723  prodmodclem3  11740  prodmodclem2a  11741  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodm1s  11766  fprodp1s  11767  fprod2dlemstep  11787  fprodcom2fi  11791  fprodsplitf  11797  odd2np1lem  12037  bitsfzolem  12118  bezoutlemmain  12165  bezoutlemeu  12174  gcdmultiple  12187  rplpwr  12194  nnwofdc  12205  nnwosdc  12206  nninfctlemfo  12207  isprm5lem  12309  isprm5  12310  pw2dvdseu  12336  hashdvds  12389  eulerthlemh  12399  reumodprminv  12422  pclemub  12456  pclemdc  12457  pceu  12464  pcmptdvds  12514  1arith  12536  4sqlem2  12558  4sqlem11  12570  4sqlem12  12571  ennnfonelemg  12620  ennnfoneleminc  12628  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemrnh  12633  ennnfonelemfun  12634  ennnfonelemdm  12637  ennnfonelemr  12640  ennnfone  12642  inffinp1  12646  ctinf  12647  nninfdclemf  12666  nninfdclemp1  12667  unbendc  12671  infpn2  12673  strsetsid  12711  mgmidmo  13015  lidrididd  13025  mndinvmod  13086  insubm  13117  dfgrp3mlem  13230  mulgaddcom  13276  mulginvcom  13277  isnsg2  13333  gsumfzconstf  13472  srgmulgass  13545  islmodd  13849  lmodvsmmulgdi  13879  rmodislmodlem  13906  rmodislmod  13907  lssats2  13970  baspartn  14286  cnpnei  14455  txdis1cn  14514  cnmptid  14517  xmetxp  14743  cncfmptc  14832  cncfmptid  14833  dedekindeulemloc  14855  dedekindicclemloc  14864  ivthinclemlr  14873  ivthinclemur  14875  ivthinclemloc  14877  ivthdec  14880  dvmptfsum  14961  plymullem1  14984  perfectlem2  15236  lgseisenlem2  15312  lgsquadlem3  15320  lgsquad  15321  lgsquad2lem2  15323  2lgslem1a  15329  spimd  15411  2spim  15412  ch2var  15413  bj-sbimedh  15417  bj-sbimeh  15418  cbvrald  15434  sumdc2  15445  bdth  15477  bdcdeq  15485  bdne  15499  bdreu  15501  bdcsn  15516  bdsep2  15532  bdsepnft  15533  bdsepnfALT  15535  bdbm1.3ii  15537  bj-nalset  15541  bj-zfpair2  15556  bj-bdfindes  15595  bj-nn0suc0  15596  bj-nntrans  15597  setindft  15611  setindis  15613  bdsetindis  15615  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619  strcoll2  15629  strcollnft  15630  strcollnfALT  15632  sscoll2  15634  nnti  15639  nnsf  15649  peano4nninf  15650  nninfsellemqall  15659  nninfomni  15663  nnnninfen  15665  trilpolemeq1  15684  tridceq  15700  redc0  15701  reap0  15702  dceqnconst  15704  dcapnconst  15705  nconstwlpolemgt0  15708