Theorem weq 1444

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

(Instead of introducing weq 1444 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 1296. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1444 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1296. 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 1296	1 wff x = y

Syntax hints:   = wceq 1296

This theorem is referenced by:  alequcoms  1461  equidqe  1477  ax4sp1  1478  equid  1641  nfequid  1642  stdpc6  1643  equcomi  1644  ax6evr  1645  equcom  1646  equcomd  1647  equcoms  1648  equtr  1649  equtrr  1650  equtr2  1651  equequ1  1652  equequ2  1653  elequ1  1654  elequ2  1655  ax11i  1656  ax10o  1657  ax10  1659  nfae  1661  hbaes  1662  hbnae  1663  nfnae  1664  hbnaes  1665  equsalh  1668  equsal  1669  dral1  1672  dral2  1673  drex2  1674  drnf1  1675  drnf2  1676  spimth  1677  spimh  1679  spimed  1682  cbv1  1686  cbv1h  1687  cbv2h  1688  cbvalh  1690  chvar  1694  sbimi  1701  sb1  1703  sb2  1704  sbequ1  1705  sbequ2  1706  sbequ12  1708  sbequ12r  1709  sbequ12a  1710  sbid  1711  stdpc4  1712  sbh  1713  sb6x  1716  sbequ5  1719  sbequ6  1720  equsb1  1722  equsb2  1723  sbiedh  1724  sbiedv  1726  sbieh  1727  equs5a  1729  drsb1  1734  exdistrfor  1735  sb4a  1736  equs45f  1737  sb6f  1738  sb5f  1739  sb4e  1740  hbsb2a  1741  hbsb2e  1742  sbcof2  1745  aev  1747  ax16  1748  dveeq2  1750  dveeq2or  1751  ax11v2  1755  ax11a2  1756  ax11b  1761  equs5  1764  equs5or  1765  sb3  1766  sb4  1767  sb4or  1768  sb4b  1769  sb4bor  1770  hbsb2  1771  nfsb2or  1772  sbequi  1774  sbequ  1775  drsb2  1776  spsbe  1777  spsbim  1778  sbequ8  1782  sbidm  1786  sb5rf  1787  sb6rf  1788  ax16i  1793  spv  1795  speiv  1797  equvin  1798  a16g  1799  a16gb  1800  a16nf  1801  sb56  1820  sb6  1821  sb5  1822  sbnv  1823  sbanv  1824  sborv  1825  sbi1v  1826  sbi2v  1827  cbval2  1851  cbvex2  1852  cbvaldva  1858  cbvexdva  1859  cbvex4v  1860  cleljust  1868  hbs1  1869  hbsbv  1872  nfsbxy  1873  nfsbxyt  1874  equsb3  1880  sbco  1897  sbcocom  1899  sbcomxyyz  1901  elsb3  1907  elsb4  1908  sb9v  1909  2sb5  1914  2sb6  1915  sbcom2v  1916  sb6a  1919  2sb5rf  1920  2sb6rf  1921  dfsb7  1922  sb7f  1923  sb7af  1924  sb10f  1926  sbel2x  1929  sbalyz  1930  sbal1yz  1932  sbal1  1933  sbexyz  1934  exsb  1939  2exsb  1940  dvelimALT  1941  dvelimfv  1942  hbsb4t  1944  nfsb4t  1945  dvelimf  1946  dvelimdf  1947  dvelimor  1949  dveeq1  1950  sbal2  1953  euf  1960  eubidh  1961  eubid  1962  hbeu1  1965  nfeu1  1966  sb8eu  1968  nfeuv  1973  sb8euh  1978  eu1  1980  mo2n  1983  euex  1985  eumo0  1986  mo23  1996  mor  1997  modc  1998  eu2  1999  eu3h  2000  mo2r  2007  mo3h  2008  mo2dc  2010  mo4f  2015  eu4  2017  moim  2019  moimv  2021  moanim  2029  mopick  2033  2eu4  2048  euequ1  2050  exists1  2051  axext3  2078  axext4  2079  bm1.1  2080  eleq1w  2155  cleqh  2194  cbvab  2217  sbab  2221  nfcjust  2223  drnfc1  2252  drnfc2  2253  dvelimdc  2255  dvelimc  2256  nfcvf  2257  cbvralf  2598  cbvrexf  2599  cbvreu  2602  cbvraldva2  2608  cbvrexdva2  2609  cbvraldva  2610  cbvrexdva  2611  cbvral2v  2612  cbvrex2v  2613  cbvral3v  2614  cbvrab  2631  vjust  2634  vex  2636  rr19.3v  2769  rr19.28v  2770  ralab2  2793  rexab2  2795  reu2  2817  reu6  2818  reu3  2819  rmo4  2822  reu4  2823  reu7  2824  reu8  2825  rmo3f  2826  rmo4f  2827  cdeqi  2839  cdeqri  2840  cdeqth  2841  cdeqnot  2842  cdeqal  2843  cdeqab  2844  cdeqim  2847  cdeqcv  2848  cdeqeq  2849  cdeqel  2850  nfccdeq  2852  sbsbc  2858  sbc8g  2861  sbcco2  2876  sbc5  2877  sbcralt  2929  sbcralg  2931  sbcreug  2933  rmo3  2944  cbvcsb  2951  sbcel12g  2960  sbceqg  2961  cbvralcsf  3004  cbvrexcsf  3005  cbvreucsf  3006  cbvrabcsf  3007  difjust  3014  unjust  3016  injust  3018  dfss2f  3030  dfdif3  3125  dfnul3  3305  dfif3  3426  preq12bg  3639  eluniab  3687  elintab  3721  int0  3724  dfiunv2  3788  cbviun  3789  cbviin  3790  cbvdisj  3854  disjiun  3862  sndisj  3863  sbcbrg  3916  cbvmptf  3954  cbvmpt  3955  axsep2  3979  bm1.3ii  3981  nalset  3990  zfpow  4031  el  4034  dtruarb  4047  copsexg  4095  opelopabsb  4111  swopo  4157  pofun  4163  issod  4170  frind  4203  zfun  4285  ruv  4394  dtru  4404  dcextest  4424  tfisi  4430  findes  4446  relop  4617  dfdmf  4660  dfrnf  4708  resiexg  4790  dfres2  4797  opabresid  4798  mptresid  4799  imai  4821  issref  4847  intasym  4849  cnvi  4869  rnxpid  4899  cnvpom  5007  nfiota1  5016  cbviota  5019  sb8iota  5021  iotaval  5025  iotanul  5029  iota4  5032  csbiotag  5042  dffun2  5059  dffun4  5060  dffun5r  5061  dffun6f  5062  dffun4f  5065  sbcfung  5073  funopg  5082  funinsn  5097  funcnveq  5111  fun11  5115  fununi  5116  funcnvuni  5117  imain  5130  isarep2  5135  brprcneu  5333  fv2  5335  elfv  5338  fv3  5363  relelfvdm  5371  fvmpt2  5422  ralrnmpt  5480  rexrnmpt  5481  ffnfvf  5496  f1veqaeq  5586  dff13f  5587  fliftfuns  5615  cbvriota  5656  csbriotag  5658  acexmid  5689  oprabidlem  5718  cbvmpt2x  5764  cbvmpt2  5765  cbvmpt2v  5766  mpt2fun  5785  abrexex2  5933  fmpt2co  6019  f1o2ndf1  6031  poxp  6035  tposoprab  6083  tfrlem3-2d  6115  tfrlemi1  6135  tfr1onlemsucfn  6143  tfr1onlemaccex  6151  tfrcllemsucfn  6156  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllembfn  6160  tfrcllemaccex  6164  dcdifsnid  6303  fnsnsplitdc  6304  funresdfunsndc  6305  eqerlem  6363  qliftfuns  6416  eroveu  6423  cbvixp  6512  mptelixpg  6531  idssen  6574  xpf1o  6640  xpmapen  6646  findcard2d  6687  nnwetri  6706  fiintim  6719  snexxph  6739  fidcenumlemim  6741  fidcenumlemrk  6743  fidcenum  6745  supmoti  6768  isoti  6782  supisoti  6785  cnvti  6794  ordiso2  6808  djuss  6841  finct  6874  ltsopi  6976  addpipqqs  7026  mulpipqqs  7029  archpr  7299  cauappcvgprlemlol  7303  cauappcvgprlemopu  7304  cauappcvgprlemupu  7305  cauappcvgprlemdisj  7307  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgprlemlim  7317  caucvgprlemlol  7326  caucvgprlemopu  7327  caucvgprlemupu  7328  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdrl  7334  caucvgprprlemcbv  7343  caucvgprprlemopu  7355  caucvgprprlemclphr  7361  caucvgprprlemexbt  7362  caucvgsrlembound  7436  caucvgsrlembnd  7443  peano1nnnn  7486  axcaucvglemres  7531  negf1o  7957  lbreu  8503  lbinf  8506  suprubex  8509  suprlubex  8510  suprleubex  8512  1nn  8531  uzind4s  9177  uzind4s2  9178  indstr  9180  supinfneg  9182  infsupneg  9183  eqreznegel  9198  lbzbi  9200  exbtwnzlemex  9810  exbtwnz  9811  rebtwn2zlemstep  9813  rebtwn2z  9815  iseqovex  10016  iseqvalcbv  10018  seq3f1olemqsum  10066  seq3f1olemp  10068  seq3f1oleml  10069  seq3distr  10079  faclbnd6  10283  fimaxq  10366  cvg1nlemres  10549  resqrexlemsqa  10588  resqrexlemex  10589  cau3lem  10678  fclim  10853  climeu  10855  cn1lem  10873  climcau  10906  climcvg1n  10909  summodclem3  10939  summodclem2a  10940  summodclem2  10941  summodc  10942  zsumdc  10943  fsum3  10946  isumz  10948  isumss2  10952  fsumsersdc  10954  fsum3ser  10956  fsumadd  10965  fsum2dlemstep  10993  fisumcom2  10997  isumshft  11049  cvgratz  11091  mertensabs  11096  odd2np1lem  11315  zsupcl  11386  infssuzex  11388  infssuzledc  11389  bezoutlemmain  11430  bezoutlemeu  11439  gcdmultiple  11452  rplpwr  11459  pw2dvdseu  11589  hashdvds  11640  strsetsid  11692  baspartn  11916  cnpnei  12086  cnmptid  12119  cncfmptc  12362  cncfmptid  12363  spimd  12390  2spim  12391  ch2var  12392  bj-sbimedh  12396  bj-sbimeh  12397  cbvrald  12412  sumdc2  12423  bdth  12446  bdcdeq  12454  bdne  12468  bdreu  12470  bdcsn  12485  bdsep2  12501  bdsepnft  12502  bdsepnfALT  12504  bdbm1.3ii  12506  bj-nalset  12510  bj-zfpair2  12525  bj-bdfindes  12568  bj-nn0suc0  12569  bj-nntrans  12570  setindft  12584  setindis  12586  bdsetindis  12588  bj-inf2vnlem3  12591  bj-inf2vnlem4  12592  strcoll2  12602  strcollnft  12603  strcollnfALT  12605  sscoll2  12607  nnti  12613  nnsf  12616  peano4nninf  12617  nninfsellemqall  12628  nninfomni  12632