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 𝑥 = 𝑦

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1364	1 wff 𝑥 = 𝑦

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  5554  fv2  5556  elfv  5559  fv3  5584  relelfvdm  5593  fvmpt2  5648  ralrnmpt  5707  rexrnmpt  5708  ffnfvf  5724  f1veqaeq  5819  dff13f  5820  fliftfuns  5848  canth  5878  cbvriota  5891  csbriotag  5893  acexmid  5924  oprabidlem  5956  cbvmpox  6004  cbvmpo  6005  cbvmpov  6006  mpofun  6028  abrexex2  6190  fmpoco  6283  f1o2ndf1  6295  poxp  6299  tposoprab  6347  tfrlem3-2d  6379  tfrlemi1  6399  tfr1onlemsucfn  6407  tfr1onlemaccex  6415  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  dcdifsnid  6571  fnsnsplitdc  6572  funresdfunsndc  6573  eqerlem  6632  qliftfuns  6687  eroveu  6694  cbvixp  6783  mptelixpg  6802  idssen  6845  pw2f1odclem  6904  xpf1o  6914  xpmapen  6920  findcard2d  6961  nnwetri  6986  fiintim  7001  snexxph  7025  fidcenumlemim  7027  fidcenumlemrk  7029  fidcenum  7031  supmoti  7068  isoti  7082  supisoti  7085  cnvti  7094  ordiso2  7110  ctssdccl  7186  finct  7191  infnninf  7199  nninfwlpoim  7254  nninfwlpo  7256  exmidontriimlem3  7308  exmidontriimlem4  7309  exmidontriim  7310  onntri13  7323  onntri51  7325  onntri3or  7330  dftap2  7336  netap  7339  2onetap  7340  2omotaplemap  7342  cc1  7350  cc2  7352  ltsopi  7406  addpipqqs  7456  mulpipqqs  7459  archpr  7729  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlemlim  7747  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdrl  7764  caucvgprprlemcbv  7773  caucvgprprlemopu  7785  caucvgprprlemclphr  7791  caucvgprprlemexbt  7792  suplocexprlemmu  7804  suplocexprlemdisj  7806  caucvgsrlembound  7880  caucvgsrlembnd  7887  suplocsrlem  7894  suplocsr  7895  peano1nnnn  7938  axcaucvglemres  7985  axpre-suploc  7988  negf1o  8427  lbreu  8991  lbinf  8994  suprubex  8997  suprlubex  8998  suprleubex  9000  1nn  9020  uzind4s  9683  uzind4s2  9684  indstr  9686  supinfneg  9688  infsupneg  9689  infregelbex  9691  eqreznegel  9707  lbzbi  9709  elpq  9742  zsupcl  10340  infssuzex  10342  infssuzledc  10343  zsupssdc  10347  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2z  10363  iseqovex  10569  iseqvalcbv  10570  seqvalcd  10572  seqovcd  10578  seq3f1olemqsum  10624  seq3f1olemp  10626  seq3f1oleml  10627  seqf1og  10632  seq3distr  10643  faclbnd6  10855  fimaxq  10938  cvg1nlemres  11169  resqrexlemsqa  11208  resqrexlemex  11209  cau3lem  11298  fclim  11478  climeu  11480  cn1lem  11498  climcau  11531  climcvg1n  11534  summodclem3  11564  summodclem2a  11565  summodclem2  11566  summodc  11567  zsumdc  11568  fsum3  11571  isumz  11573  isumss2  11577  fsumsersdc  11579  fsum3ser  11581  fsumadd  11590  fsum2dlemstep  11618  fisumcom2  11622  isumshft  11674  cvgratz  11716  mertensabs  11721  prodfdivap  11731  cbvprod  11742  prodmodclem3  11759  prodmodclem2a  11760  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodm1s  11785  fprodp1s  11786  fprod2dlemstep  11806  fprodcom2fi  11810  fprodsplitf  11816  odd2np1lem  12056  bitsfzolem  12138  bezoutlemmain  12192  bezoutlemeu  12201  gcdmultiple  12214  rplpwr  12221  nnwofdc  12232  nnwosdc  12233  nninfctlemfo  12234  isprm5lem  12336  isprm5  12337  pw2dvdseu  12363  hashdvds  12416  eulerthlemh  12426  reumodprminv  12449  pclemub  12483  pclemdc  12484  pceu  12491  pcmptdvds  12541  1arith  12563  4sqlem2  12585  4sqlem11  12597  4sqlem12  12598  ennnfonelemg  12647  ennnfoneleminc  12655  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemrnh  12660  ennnfonelemfun  12661  ennnfonelemdm  12664  ennnfonelemr  12667  ennnfone  12669  inffinp1  12673  ctinf  12674  nninfdclemf  12693  nninfdclemp1  12694  unbendc  12698  infpn2  12700  strsetsid  12738  mgmidmo  13076  lidrididd  13086  mndinvmod  13149  insubm  13189  dfgrp3mlem  13302  mulgaddcom  13354  mulginvcom  13355  isnsg2  13411  gsumfzconstf  13550  srgmulgass  13623  islmodd  13927  lmodvsmmulgdi  13957  rmodislmodlem  13984  rmodislmod  13985  lssats2  14048  mplsubgfilemcl  14333  baspartn  14394  cnpnei  14563  txdis1cn  14622  cnmptid  14625  xmetxp  14851  cncfmptc  14940  cncfmptid  14941  dedekindeulemloc  14963  dedekindicclemloc  14972  ivthinclemlr  14981  ivthinclemur  14983  ivthinclemloc  14985  ivthdec  14988  dvmptfsum  15069  plymullem1  15092  perfectlem2  15344  lgseisenlem2  15420  lgsquadlem3  15428  lgsquad  15429  lgsquad2lem2  15431  2lgslem1a  15437  spimd  15519  2spim  15520  ch2var  15521  bj-sbimedh  15525  bj-sbimeh  15526  cbvrald  15542  sumdc2  15553  bdth  15585  bdcdeq  15593  bdne  15607  bdreu  15609  bdcsn  15624  bdsep2  15640  bdsepnft  15641  bdsepnfALT  15643  bdbm1.3ii  15645  bj-nalset  15649  bj-zfpair2  15664  bj-bdfindes  15703  bj-nn0suc0  15704  bj-nntrans  15705  setindft  15719  setindis  15721  bdsetindis  15723  bj-inf2vnlem3  15726  bj-inf2vnlem4  15727  strcoll2  15737  strcollnft  15738  strcollnfALT  15740  sscoll2  15742  nnti  15747  2omap  15750  nnsf  15760  peano4nninf  15761  nninfsellemqall  15770  nninfomni  15774  nnnninfen  15776  trilpolemeq1  15797  tridceq  15813  redc0  15814  reap0  15815  dceqnconst  15817  dcapnconst  15818  nconstwlpolemgt0  15821