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  2899  rr19.28v  2900  ralab2  2924  rexab2  2926  reu2  2948  reu6  2949  reu3  2950  rmo4  2953  reu4  2954  reu7  2955  reu8  2956  rmo3f  2957  rmo4f  2958  cdeqi  2970  cdeqri  2971  cdeqth  2972  cdeqnot  2973  cdeqal  2974  cdeqab  2975  cdeqim  2978  cdeqcv  2979  cdeqeq  2980  cdeqel  2981  nfccdeq  2983  sbsbc  2989  sbc8g  2993  sbcco2  3008  sbc5  3009  sbcralt  3062  sbcralg  3064  sbcreug  3066  rmo3  3077  cbvcsbw  3084  cbvcsb  3085  csbcow  3091  sbcel12g  3095  sbceqg  3096  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  difjust  3154  unjust  3156  injust  3158  dfss2f  3170  dfdif3  3269  dfnul3  3449  dfif3  3570  preq12bg  3799  eluniab  3847  elintab  3881  int0  3884  dfiunv2  3948  cbviun  3949  cbviin  3950  cbvdisj  4016  disjiun  4024  sndisj  4025  sbcbrg  4083  cbvmptf  4123  cbvmpt  4124  axsep2  4148  bm1.3ii  4150  nalset  4159  zfpow  4204  el  4207  dtruarb  4220  copsexg  4273  opelopabsb  4290  swopo  4337  pofun  4343  issod  4350  frind  4383  zfun  4465  ruv  4582  dtru  4592  dcextest  4613  tfisi  4619  findes  4635  relop  4812  dfdmf  4855  dfrnf  4903  resiexg  4987  dfres2  4994  opabresid  4995  mptresid  4996  imai  5021  issref  5048  intasym  5050  cnvi  5070  rnxpid  5100  cnvpom  5208  nfiota1  5217  cbviota  5220  sb8iota  5222  iotaval  5226  iotanul  5230  iota4  5234  eliota  5242  eliotaeu  5243  csbiotag  5247  dffun2  5264  dffun4  5265  dffun5r  5266  dffun6f  5267  dffun4f  5270  sbcfung  5278  funopg  5288  funinsn  5303  funcnveq  5317  fun11  5321  fununi  5322  funcnvuni  5323  imain  5336  isarep2  5341  brprcneu  5547  fv2  5549  elfv  5552  fv3  5577  relelfvdm  5586  fvmpt2  5641  ralrnmpt  5700  rexrnmpt  5701  ffnfvf  5717  f1veqaeq  5812  dff13f  5813  fliftfuns  5841  canth  5871  cbvriota  5884  csbriotag  5886  acexmid  5917  oprabidlem  5949  cbvmpox  5996  cbvmpo  5997  cbvmpov  5998  mpofun  6020  abrexex2  6176  fmpoco  6269  f1o2ndf1  6281  poxp  6285  tposoprab  6333  tfrlem3-2d  6365  tfrlemi1  6385  tfr1onlemsucfn  6393  tfr1onlemaccex  6401  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemaccex  6414  dcdifsnid  6557  fnsnsplitdc  6558  funresdfunsndc  6559  eqerlem  6618  qliftfuns  6673  eroveu  6680  cbvixp  6769  mptelixpg  6788  idssen  6831  pw2f1odclem  6890  xpf1o  6900  xpmapen  6906  findcard2d  6947  nnwetri  6972  fiintim  6985  snexxph  7009  fidcenumlemim  7011  fidcenumlemrk  7013  fidcenum  7015  supmoti  7052  isoti  7066  supisoti  7069  cnvti  7078  ordiso2  7094  ctssdccl  7170  finct  7175  infnninf  7183  nninfwlpoim  7237  nninfwlpo  7238  exmidontriimlem3  7283  exmidontriimlem4  7284  exmidontriim  7285  onntri13  7298  onntri51  7300  onntri3or  7305  dftap2  7311  netap  7314  2onetap  7315  2omotaplemap  7317  cc1  7325  cc2  7327  ltsopi  7380  addpipqqs  7430  mulpipqqs  7433  archpr  7703  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlemlim  7721  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdrl  7738  caucvgprprlemcbv  7747  caucvgprprlemopu  7759  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  suplocexprlemmu  7778  suplocexprlemdisj  7780  caucvgsrlembound  7854  caucvgsrlembnd  7861  suplocsrlem  7868  suplocsr  7869  peano1nnnn  7912  axcaucvglemres  7959  axpre-suploc  7962  negf1o  8401  lbreu  8964  lbinf  8967  suprubex  8970  suprlubex  8971  suprleubex  8973  1nn  8993  uzind4s  9655  uzind4s2  9656  indstr  9658  supinfneg  9660  infsupneg  9661  infregelbex  9663  eqreznegel  9679  lbzbi  9681  elpq  9714  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2z  10323  iseqovex  10529  iseqvalcbv  10530  seqvalcd  10532  seqovcd  10538  seq3f1olemqsum  10584  seq3f1olemp  10586  seq3f1oleml  10587  seqf1og  10592  seq3distr  10603  faclbnd6  10815  fimaxq  10898  cvg1nlemres  11129  resqrexlemsqa  11168  resqrexlemex  11169  cau3lem  11258  fclim  11437  climeu  11439  cn1lem  11457  climcau  11490  climcvg1n  11493  summodclem3  11523  summodclem2a  11524  summodclem2  11525  summodc  11526  zsumdc  11527  fsum3  11530  isumz  11532  isumss2  11536  fsumsersdc  11538  fsum3ser  11540  fsumadd  11549  fsum2dlemstep  11577  fisumcom2  11581  isumshft  11633  cvgratz  11675  mertensabs  11680  prodfdivap  11690  cbvprod  11701  prodmodclem3  11718  prodmodclem2a  11719  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodm1s  11744  fprodp1s  11745  fprod2dlemstep  11765  fprodcom2fi  11769  fprodsplitf  11775  odd2np1lem  12013  zsupcl  12084  infssuzex  12086  infssuzledc  12087  zsupssdc  12091  bezoutlemmain  12135  bezoutlemeu  12144  gcdmultiple  12157  rplpwr  12164  nnwofdc  12175  nnwosdc  12176  nninfctlemfo  12177  isprm5lem  12279  isprm5  12280  pw2dvdseu  12306  hashdvds  12359  eulerthlemh  12369  reumodprminv  12391  pclemub  12425  pclemdc  12426  pceu  12433  pcmptdvds  12483  1arith  12505  4sqlem2  12527  4sqlem11  12539  4sqlem12  12540  ennnfonelemg  12560  ennnfoneleminc  12568  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemrnh  12573  ennnfonelemfun  12574  ennnfonelemdm  12577  ennnfonelemr  12580  ennnfone  12582  inffinp1  12586  ctinf  12587  nninfdclemf  12606  nninfdclemp1  12607  unbendc  12611  infpn2  12613  strsetsid  12651  mgmidmo  12955  lidrididd  12965  mndinvmod  13026  insubm  13057  dfgrp3mlem  13170  mulgaddcom  13216  mulginvcom  13217  isnsg2  13273  gsumfzconstf  13412  srgmulgass  13485  islmodd  13789  lmodvsmmulgdi  13819  rmodislmodlem  13846  rmodislmod  13847  lssats2  13910  baspartn  14218  cnpnei  14387  txdis1cn  14446  cnmptid  14449  xmetxp  14675  cncfmptc  14750  cncfmptid  14751  dedekindeulemloc  14773  dedekindicclemloc  14782  ivthinclemlr  14791  ivthinclemur  14793  ivthinclemloc  14795  ivthdec  14798  plymullem1  14894  lgseisenlem2  15187  spimd  15257  2spim  15258  ch2var  15259  bj-sbimedh  15263  bj-sbimeh  15264  cbvrald  15280  sumdc2  15291  bdth  15323  bdcdeq  15331  bdne  15345  bdreu  15347  bdcsn  15362  bdsep2  15378  bdsepnft  15379  bdsepnfALT  15381  bdbm1.3ii  15383  bj-nalset  15387  bj-zfpair2  15402  bj-bdfindes  15441  bj-nn0suc0  15442  bj-nntrans  15443  setindft  15457  setindis  15459  bdsetindis  15461  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465  strcoll2  15475  strcollnft  15476  strcollnfALT  15478  sscoll2  15480  nnti  15485  nnsf  15495  peano4nninf  15496  nninfsellemqall  15505  nninfomni  15509  nnnninfen  15511  trilpolemeq1  15530  tridceq  15546  redc0  15547  reap0  15548  dceqnconst  15550  dcapnconst  15551  nconstwlpolemgt0  15554