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  7253  nninfwlpo  7254  exmidontriimlem3  7306  exmidontriimlem4  7307  exmidontriim  7308  onntri13  7321  onntri51  7323  onntri3or  7328  dftap2  7334  netap  7337  2onetap  7338  2omotaplemap  7340  cc1  7348  cc2  7350  ltsopi  7404  addpipqqs  7454  mulpipqqs  7457  archpr  7727  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlemlim  7745  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdrl  7762  caucvgprprlemcbv  7771  caucvgprprlemopu  7783  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  suplocexprlemmu  7802  suplocexprlemdisj  7804  caucvgsrlembound  7878  caucvgsrlembnd  7885  suplocsrlem  7892  suplocsr  7893  peano1nnnn  7936  axcaucvglemres  7983  axpre-suploc  7986  negf1o  8425  lbreu  8989  lbinf  8992  suprubex  8995  suprlubex  8996  suprleubex  8998  1nn  9018  uzind4s  9681  uzind4s2  9682  indstr  9684  supinfneg  9686  infsupneg  9687  infregelbex  9689  eqreznegel  9705  lbzbi  9707  elpq  9740  zsupcl  10338  infssuzex  10340  infssuzledc  10341  zsupssdc  10345  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2z  10361  iseqovex  10567  iseqvalcbv  10568  seqvalcd  10570  seqovcd  10576  seq3f1olemqsum  10622  seq3f1olemp  10624  seq3f1oleml  10625  seqf1og  10630  seq3distr  10641  faclbnd6  10853  fimaxq  10936  cvg1nlemres  11167  resqrexlemsqa  11206  resqrexlemex  11207  cau3lem  11296  fclim  11476  climeu  11478  cn1lem  11496  climcau  11529  climcvg1n  11532  summodclem3  11562  summodclem2a  11563  summodclem2  11564  summodc  11565  zsumdc  11566  fsum3  11569  isumz  11571  isumss2  11575  fsumsersdc  11577  fsum3ser  11579  fsumadd  11588  fsum2dlemstep  11616  fisumcom2  11620  isumshft  11672  cvgratz  11714  mertensabs  11719  prodfdivap  11729  cbvprod  11740  prodmodclem3  11757  prodmodclem2a  11758  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodm1s  11783  fprodp1s  11784  fprod2dlemstep  11804  fprodcom2fi  11808  fprodsplitf  11814  odd2np1lem  12054  bitsfzolem  12136  bezoutlemmain  12190  bezoutlemeu  12199  gcdmultiple  12212  rplpwr  12219  nnwofdc  12230  nnwosdc  12231  nninfctlemfo  12232  isprm5lem  12334  isprm5  12335  pw2dvdseu  12361  hashdvds  12414  eulerthlemh  12424  reumodprminv  12447  pclemub  12481  pclemdc  12482  pceu  12489  pcmptdvds  12539  1arith  12561  4sqlem2  12583  4sqlem11  12595  4sqlem12  12596  ennnfonelemg  12645  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemrnh  12658  ennnfonelemfun  12659  ennnfonelemdm  12662  ennnfonelemr  12665  ennnfone  12667  inffinp1  12671  ctinf  12672  nninfdclemf  12691  nninfdclemp1  12692  unbendc  12696  infpn2  12698  strsetsid  12736  mgmidmo  13074  lidrididd  13084  mndinvmod  13147  insubm  13187  dfgrp3mlem  13300  mulgaddcom  13352  mulginvcom  13353  isnsg2  13409  gsumfzconstf  13548  srgmulgass  13621  islmodd  13925  lmodvsmmulgdi  13955  rmodislmodlem  13982  rmodislmod  13983  lssats2  14046  baspartn  14370  cnpnei  14539  txdis1cn  14598  cnmptid  14601  xmetxp  14827  cncfmptc  14916  cncfmptid  14917  dedekindeulemloc  14939  dedekindicclemloc  14948  ivthinclemlr  14957  ivthinclemur  14959  ivthinclemloc  14961  ivthdec  14964  dvmptfsum  15045  plymullem1  15068  perfectlem2  15320  lgseisenlem2  15396  lgsquadlem3  15404  lgsquad  15405  lgsquad2lem2  15407  2lgslem1a  15413  spimd  15495  2spim  15496  ch2var  15497  bj-sbimedh  15501  bj-sbimeh  15502  cbvrald  15518  sumdc2  15529  bdth  15561  bdcdeq  15569  bdne  15583  bdreu  15585  bdcsn  15600  bdsep2  15616  bdsepnft  15617  bdsepnfALT  15619  bdbm1.3ii  15621  bj-nalset  15625  bj-zfpair2  15640  bj-bdfindes  15679  bj-nn0suc0  15680  bj-nntrans  15681  setindft  15695  setindis  15697  bdsetindis  15699  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703  strcoll2  15713  strcollnft  15714  strcollnfALT  15716  sscoll2  15718  nnti  15723  2omap  15726  nnsf  15736  peano4nninf  15737  nninfsellemqall  15746  nninfomni  15750  nnnninfen  15752  trilpolemeq1  15771  tridceq  15787  redc0  15788  reap0  15789  dceqnconst  15791  dcapnconst  15792  nconstwlpolemgt0  15795