Theorem weq 1514

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

(Instead of introducing weq 1514 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 1514 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  1527  equidqe  1543  ax4sp1  1544  spimfv  1710  chvarfv  1711  equid  1712  nfequid  1713  stdpc6  1714  equcomi  1715  ax6evr  1716  equcom  1717  equcomd  1718  equcoms  1719  equtr  1720  equtrr  1721  equtr2  1722  equequ1  1723  equequ2  1724  ax11i  1725  ax10o  1726  ax10  1728  nfae  1730  hbaes  1731  hbnae  1732  nfnae  1733  hbnaes  1734  equsalh  1737  equsal  1738  dral1  1741  dral2  1742  drex2  1743  drnf1  1744  drnf2  1745  spimth  1746  spimh  1748  spimed  1751  cbv1  1756  cbv1h  1757  cbv1v  1758  cbv2h  1759  cbv2w  1761  cbvalv1  1762  cbvexv1  1763  cbvalh  1764  chvar  1768  sbimi  1775  sb1  1777  sb2  1778  sbequ1  1779  sbequ2  1780  sbequ12  1782  sbequ12r  1783  sbequ12a  1784  sbid  1785  stdpc4  1786  sbh  1787  sb6x  1790  sbequ5  1793  sbequ6  1794  equsb1  1796  equsb2  1797  sbiedh  1798  sbiedv  1800  sbieh  1801  equsalv  1804  equs5a  1805  drsb1  1810  exdistrfor  1811  sb4a  1812  equs45f  1813  sb6f  1814  sb5f  1815  sb4e  1816  hbsb2a  1817  hbsb2e  1818  sbcof2  1821  aev  1823  ax16  1824  dveeq2  1826  dveeq2or  1827  ax11v2  1831  ax11a2  1832  ax11b  1837  equs5  1840  equs5or  1841  sb3  1842  sb4  1843  sb4or  1844  sb4b  1845  sb4bor  1846  hbsb2  1847  nfsb2or  1848  sbequi  1850  sbequ  1851  drsb2  1852  spsbe  1853  spsbim  1854  sbequ8  1858  sbidm  1862  sb5rf  1863  sb6rf  1864  ax16i  1869  spv  1871  speiv  1873  equvin  1874  a16g  1875  a16gb  1876  a16nf  1877  sb56  1897  sb6  1898  sb5  1899  sbnv  1900  sbanv  1901  sborv  1902  sbi1v  1903  sbi2v  1904  cbvalvw  1931  cbvexvw  1932  cbval2  1933  cbvex2  1934  cbvaldva  1940  cbvexdva  1941  cbvaldvaw  1942  cbval2vw  1944  cbvex2vw  1945  cbvex4v  1946  hbs1  1954  hbsbv  1957  nfsbxy  1958  nfsbxyt  1959  nfsbv  1963  equsb3  1967  sbco  1984  sbcocom  1986  sbcomxyyz  1988  sb9v  1994  2sb5  1999  2sb6  2000  sbcom2v  2001  sb6a  2004  2sb5rf  2005  2sb6rf  2006  dfsb7  2007  sb7f  2008  sb7af  2009  sb10f  2011  sbel2x  2014  sbalyz  2015  sbal1yz  2017  sbal1  2018  sbexyz  2019  exsb  2024  2exsb  2025  dvelimALT  2026  dvelimfv  2027  hbsb4t  2029  nfsb4t  2030  dvelimf  2031  dvelimdf  2032  dvelimor  2034  dveeq1  2035  sbal2  2036  euf  2047  eubidh  2048  eubid  2049  hbeu1  2052  nfeu1  2053  sb8eu  2055  nfeuv  2060  sb8euh  2065  eu1  2067  mo2n  2070  euex  2072  eumo0  2073  mo23  2083  mor  2084  modc  2085  eu2  2086  eu3h  2087  mo2r  2094  mo3h  2095  mo2dc  2097  mo4f  2102  eu4  2104  moim  2106  moimv  2108  moanim  2116  mopick  2120  2eu4  2135  euequ1  2137  exists1  2138  elequ1  2168  elequ2  2169  cleljust  2170  elsb1  2171  elsb2  2172  axext3  2176  axext4  2177  bm1.1  2178  eleq1w  2254  cleqh  2293  cbvabw  2316  cbvab  2317  sbab  2321  nfcjust  2324  drnfc1  2353  drnfc2  2354  nfabdw  2355  dvelimdc  2357  dvelimc  2358  nfcvf  2359  cbvralfw  2716  cbvrexfw  2717  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvralvw  2730  cbvrexvw  2731  cbvreuvw  2732  cbvraldva2  2733  cbvrexdva2  2734  cbvraldva  2735  cbvrexdva  2736  cbvral2vw  2737  cbvrex2vw  2738  cbvral2v  2739  cbvrex2v  2740  cbvral3v  2741  sbralie  2744  cbvrab  2758  vjust  2761  vex  2763  rr19.3v  2900  rr19.28v  2901  ralab2  2925  rexab2  2927  reu2  2949  reu6  2950  reu3  2951  rmo4  2954  reu4  2955  reu7  2956  reu8  2957  rmo3f  2958  rmo4f  2959  cdeqi  2971  cdeqri  2972  cdeqth  2973  cdeqnot  2974  cdeqal  2975  cdeqab  2976  cdeqim  2979  cdeqcv  2980  cdeqeq  2981  cdeqel  2982  nfccdeq  2984  sbsbc  2990  sbc8g  2994  sbcco2  3009  sbc5  3010  sbcralt  3063  sbcralg  3065  sbcreug  3067  rmo3  3078  cbvcsbw  3085  cbvcsb  3086  csbcow  3092  sbcel12g  3096  sbceqg  3097  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  difjust  3155  unjust  3157  injust  3159  dfss2f  3171  dfdif3  3270  dfnul3  3450  dfif3  3571  preq12bg  3800  eluniab  3848  elintab  3882  int0  3885  dfiunv2  3949  cbviun  3950  cbviin  3951  cbvdisj  4017  disjiun  4025  sndisj  4026  sbcbrg  4084  cbvmptf  4124  cbvmpt  4125  axsep2  4149  bm1.3ii  4151  nalset  4160  zfpow  4205  el  4208  dtruarb  4221  copsexg  4274  opelopabsb  4291  swopo  4338  pofun  4344  issod  4351  frind  4384  zfun  4466  ruv  4583  dtru  4593  dcextest  4614  tfisi  4620  findes  4636  relop  4813  dfdmf  4856  dfrnf  4904  resiexg  4988  dfres2  4995  opabresid  4996  mptresid  4997  imai  5022  issref  5049  intasym  5051  cnvi  5071  rnxpid  5101  cnvpom  5209  nfiota1  5218  cbviota  5221  sb8iota  5223  iotaval  5227  iotanul  5231  iota4  5235  eliota  5243  eliotaeu  5244  csbiotag  5248  dffun2  5265  dffun4  5266  dffun5r  5267  dffun6f  5268  dffun4f  5271  sbcfung  5279  funopg  5289  funinsn  5304  funcnveq  5318  fun11  5322  fununi  5323  funcnvuni  5324  imain  5337  isarep2  5342  brprcneu  5548  fv2  5550  elfv  5553  fv3  5578  relelfvdm  5587  fvmpt2  5642  ralrnmpt  5701  rexrnmpt  5702  ffnfvf  5718  f1veqaeq  5813  dff13f  5814  fliftfuns  5842  canth  5872  cbvriota  5885  csbriotag  5887  acexmid  5918  oprabidlem  5950  cbvmpox  5997  cbvmpo  5998  cbvmpov  5999  mpofun  6021  abrexex2  6178  fmpoco  6271  f1o2ndf1  6283  poxp  6287  tposoprab  6335  tfrlem3-2d  6367  tfrlemi1  6387  tfr1onlemsucfn  6395  tfr1onlemaccex  6403  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemaccex  6416  dcdifsnid  6559  fnsnsplitdc  6560  funresdfunsndc  6561  eqerlem  6620  qliftfuns  6675  eroveu  6682  cbvixp  6771  mptelixpg  6790  idssen  6833  pw2f1odclem  6892  xpf1o  6902  xpmapen  6908  findcard2d  6949  nnwetri  6974  fiintim  6987  snexxph  7011  fidcenumlemim  7013  fidcenumlemrk  7015  fidcenum  7017  supmoti  7054  isoti  7068  supisoti  7071  cnvti  7080  ordiso2  7096  ctssdccl  7172  finct  7177  infnninf  7185  nninfwlpoim  7239  nninfwlpo  7240  exmidontriimlem3  7285  exmidontriimlem4  7286  exmidontriim  7287  onntri13  7300  onntri51  7302  onntri3or  7307  dftap2  7313  netap  7316  2onetap  7317  2omotaplemap  7319  cc1  7327  cc2  7329  ltsopi  7382  addpipqqs  7432  mulpipqqs  7435  archpr  7705  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlemlim  7723  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdrl  7740  caucvgprprlemcbv  7749  caucvgprprlemopu  7761  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  suplocexprlemmu  7780  suplocexprlemdisj  7782  caucvgsrlembound  7856  caucvgsrlembnd  7863  suplocsrlem  7870  suplocsr  7871  peano1nnnn  7914  axcaucvglemres  7961  axpre-suploc  7964  negf1o  8403  lbreu  8966  lbinf  8969  suprubex  8972  suprlubex  8973  suprleubex  8975  1nn  8995  uzind4s  9658  uzind4s2  9659  indstr  9661  supinfneg  9663  infsupneg  9664  infregelbex  9666  eqreznegel  9682  lbzbi  9684  elpq  9717  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2z  10326  iseqovex  10532  iseqvalcbv  10533  seqvalcd  10535  seqovcd  10541  seq3f1olemqsum  10587  seq3f1olemp  10589  seq3f1oleml  10590  seqf1og  10595  seq3distr  10606  faclbnd6  10818  fimaxq  10901  cvg1nlemres  11132  resqrexlemsqa  11171  resqrexlemex  11172  cau3lem  11261  fclim  11440  climeu  11442  cn1lem  11460  climcau  11493  climcvg1n  11496  summodclem3  11526  summodclem2a  11527  summodclem2  11528  summodc  11529  zsumdc  11530  fsum3  11533  isumz  11535  isumss2  11539  fsumsersdc  11541  fsum3ser  11543  fsumadd  11552  fsum2dlemstep  11580  fisumcom2  11584  isumshft  11636  cvgratz  11678  mertensabs  11683  prodfdivap  11693  cbvprod  11704  prodmodclem3  11721  prodmodclem2a  11722  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodm1s  11747  fprodp1s  11748  fprod2dlemstep  11768  fprodcom2fi  11772  fprodsplitf  11778  odd2np1lem  12016  zsupcl  12087  infssuzex  12089  infssuzledc  12090  zsupssdc  12094  bezoutlemmain  12138  bezoutlemeu  12147  gcdmultiple  12160  rplpwr  12167  nnwofdc  12178  nnwosdc  12179  nninfctlemfo  12180  isprm5lem  12282  isprm5  12283  pw2dvdseu  12309  hashdvds  12362  eulerthlemh  12372  reumodprminv  12394  pclemub  12428  pclemdc  12429  pceu  12436  pcmptdvds  12486  1arith  12508  4sqlem2  12530  4sqlem11  12542  4sqlem12  12543  ennnfonelemg  12563  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemrnh  12576  ennnfonelemfun  12577  ennnfonelemdm  12580  ennnfonelemr  12583  ennnfone  12585  inffinp1  12589  ctinf  12590  nninfdclemf  12609  nninfdclemp1  12610  unbendc  12614  infpn2  12616  strsetsid  12654  mgmidmo  12958  lidrididd  12968  mndinvmod  13029  insubm  13060  dfgrp3mlem  13173  mulgaddcom  13219  mulginvcom  13220  isnsg2  13276  gsumfzconstf  13415  srgmulgass  13488  islmodd  13792  lmodvsmmulgdi  13822  rmodislmodlem  13849  rmodislmod  13850  lssats2  13913  baspartn  14229  cnpnei  14398  txdis1cn  14457  cnmptid  14460  xmetxp  14686  cncfmptc  14775  cncfmptid  14776  dedekindeulemloc  14798  dedekindicclemloc  14807  ivthinclemlr  14816  ivthinclemur  14818  ivthinclemloc  14820  ivthdec  14823  dvmptfsum  14904  plymullem1  14927  lgseisenlem2  15228  lgsquadlem3  15236  lgsquad  15237  lgsquad2lem2  15239  2lgslem1a  15245  spimd  15327  2spim  15328  ch2var  15329  bj-sbimedh  15333  bj-sbimeh  15334  cbvrald  15350  sumdc2  15361  bdth  15393  bdcdeq  15401  bdne  15415  bdreu  15417  bdcsn  15432  bdsep2  15448  bdsepnft  15449  bdsepnfALT  15451  bdbm1.3ii  15453  bj-nalset  15457  bj-zfpair2  15472  bj-bdfindes  15511  bj-nn0suc0  15512  bj-nntrans  15513  setindft  15527  setindis  15529  bdsetindis  15531  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535  strcoll2  15545  strcollnft  15546  strcollnfALT  15548  sscoll2  15550  nnti  15555  nnsf  15565  peano4nninf  15566  nninfsellemqall  15575  nninfomni  15579  nnnninfen  15581  trilpolemeq1  15600  tridceq  15616  redc0  15617  reap0  15618  dceqnconst  15620  dcapnconst  15621  nconstwlpolemgt0  15624