Theorem weq 1460

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

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

Syntax hints:   = wceq 1312

This theorem is referenced by:  alequcoms  1477  equidqe  1493  ax4sp1  1494  equid  1658  nfequid  1659  stdpc6  1660  equcomi  1661  ax6evr  1662  equcom  1663  equcomd  1664  equcoms  1665  equtr  1666  equtrr  1667  equtr2  1668  equequ1  1669  equequ2  1670  elequ1  1671  elequ2  1672  ax11i  1673  ax10o  1674  ax10  1676  nfae  1678  hbaes  1679  hbnae  1680  nfnae  1681  hbnaes  1682  equsalh  1685  equsal  1686  dral1  1689  dral2  1690  drex2  1691  drnf1  1692  drnf2  1693  spimth  1694  spimh  1696  spimed  1699  cbv1  1703  cbv1h  1704  cbv2h  1705  cbvalh  1707  chvar  1711  sbimi  1718  sb1  1720  sb2  1721  sbequ1  1722  sbequ2  1723  sbequ12  1725  sbequ12r  1726  sbequ12a  1727  sbid  1728  stdpc4  1729  sbh  1730  sb6x  1733  sbequ5  1736  sbequ6  1737  equsb1  1739  equsb2  1740  sbiedh  1741  sbiedv  1743  sbieh  1744  equs5a  1746  drsb1  1751  exdistrfor  1752  sb4a  1753  equs45f  1754  sb6f  1755  sb5f  1756  sb4e  1757  hbsb2a  1758  hbsb2e  1759  sbcof2  1762  aev  1764  ax16  1765  dveeq2  1767  dveeq2or  1768  ax11v2  1772  ax11a2  1773  ax11b  1778  equs5  1781  equs5or  1782  sb3  1783  sb4  1784  sb4or  1785  sb4b  1786  sb4bor  1787  hbsb2  1788  nfsb2or  1789  sbequi  1791  sbequ  1792  drsb2  1793  spsbe  1794  spsbim  1795  sbequ8  1799  sbidm  1803  sb5rf  1804  sb6rf  1805  ax16i  1810  spv  1812  speiv  1814  equvin  1815  a16g  1816  a16gb  1817  a16nf  1818  sb56  1837  sb6  1838  sb5  1839  sbnv  1840  sbanv  1841  sborv  1842  sbi1v  1843  sbi2v  1844  cbval2  1869  cbvex2  1870  cbvaldva  1876  cbvexdva  1877  cbvex4v  1878  cleljust  1886  hbs1  1887  hbsbv  1890  nfsbxy  1891  nfsbxyt  1892  equsb3  1898  sbco  1915  sbcocom  1917  sbcomxyyz  1919  elsb3  1925  elsb4  1926  sb9v  1927  2sb5  1932  2sb6  1933  sbcom2v  1934  sb6a  1937  2sb5rf  1938  2sb6rf  1939  dfsb7  1940  sb7f  1941  sb7af  1942  sb10f  1944  sbel2x  1947  sbalyz  1948  sbal1yz  1950  sbal1  1951  sbexyz  1952  exsb  1957  2exsb  1958  dvelimALT  1959  dvelimfv  1960  hbsb4t  1962  nfsb4t  1963  dvelimf  1964  dvelimdf  1965  dvelimor  1967  dveeq1  1968  sbal2  1971  euf  1978  eubidh  1979  eubid  1980  hbeu1  1983  nfeu1  1984  sb8eu  1986  nfeuv  1991  sb8euh  1996  eu1  1998  mo2n  2001  euex  2003  eumo0  2004  mo23  2014  mor  2015  modc  2016  eu2  2017  eu3h  2018  mo2r  2025  mo3h  2026  mo2dc  2028  mo4f  2033  eu4  2035  moim  2037  moimv  2039  moanim  2047  mopick  2051  2eu4  2066  euequ1  2068  exists1  2069  axext3  2096  axext4  2097  bm1.1  2098  eleq1w  2173  cleqh  2212  cbvab  2235  sbab  2239  nfcjust  2241  drnfc1  2270  drnfc2  2271  dvelimdc  2273  dvelimc  2274  nfcvf  2275  cbvralf  2620  cbvrexf  2621  cbvreu  2624  cbvraldva2  2630  cbvrexdva2  2631  cbvraldva  2632  cbvrexdva  2633  cbvral2v  2634  cbvrex2v  2635  cbvral3v  2636  sbralie  2639  cbvrab  2653  vjust  2656  vex  2658  rr19.3v  2791  rr19.28v  2792  ralab2  2815  rexab2  2817  reu2  2839  reu6  2840  reu3  2841  rmo4  2844  reu4  2845  reu7  2846  reu8  2847  rmo3f  2848  rmo4f  2849  cdeqi  2861  cdeqri  2862  cdeqth  2863  cdeqnot  2864  cdeqal  2865  cdeqab  2866  cdeqim  2869  cdeqcv  2870  cdeqeq  2871  cdeqel  2872  nfccdeq  2874  sbsbc  2880  sbc8g  2883  sbcco2  2898  sbc5  2899  sbcralt  2951  sbcralg  2953  sbcreug  2955  rmo3  2966  cbvcsb  2973  sbcel12g  2982  sbceqg  2983  cbvralcsf  3026  cbvrexcsf  3027  cbvreucsf  3028  cbvrabcsf  3029  difjust  3036  unjust  3038  injust  3040  dfss2f  3052  dfdif3  3150  dfnul3  3330  dfif3  3451  preq12bg  3664  eluniab  3712  elintab  3746  int0  3749  dfiunv2  3813  cbviun  3814  cbviin  3815  cbvdisj  3880  disjiun  3888  sndisj  3889  sbcbrg  3942  cbvmptf  3980  cbvmpt  3981  axsep2  4005  bm1.3ii  4007  nalset  4016  zfpow  4057  el  4060  dtruarb  4073  copsexg  4124  opelopabsb  4140  swopo  4186  pofun  4192  issod  4199  frind  4232  zfun  4314  ruv  4423  dtru  4433  dcextest  4453  tfisi  4459  findes  4475  relop  4647  dfdmf  4690  dfrnf  4738  resiexg  4820  dfres2  4827  opabresid  4828  mptresid  4829  imai  4851  issref  4877  intasym  4879  cnvi  4899  rnxpid  4929  cnvpom  5037  nfiota1  5046  cbviota  5049  sb8iota  5051  iotaval  5055  iotanul  5059  iota4  5062  csbiotag  5072  dffun2  5089  dffun4  5090  dffun5r  5091  dffun6f  5092  dffun4f  5095  sbcfung  5103  funopg  5113  funinsn  5128  funcnveq  5142  fun11  5146  fununi  5147  funcnvuni  5148  imain  5161  isarep2  5166  brprcneu  5366  fv2  5368  elfv  5371  fv3  5396  relelfvdm  5405  fvmpt2  5456  ralrnmpt  5514  rexrnmpt  5515  ffnfvf  5531  f1veqaeq  5622  dff13f  5623  fliftfuns  5651  cbvriota  5692  csbriotag  5694  acexmid  5725  oprabidlem  5754  cbvmpox  5801  cbvmpo  5802  cbvmpov  5803  mpofun  5825  abrexex2  5973  fmpoco  6064  f1o2ndf1  6076  poxp  6080  tposoprab  6128  tfrlem3-2d  6160  tfrlemi1  6180  tfr1onlemsucfn  6188  tfr1onlemaccex  6196  tfrcllemsucfn  6201  tfrcllemsucaccv  6202  tfrcllembxssdm  6204  tfrcllembfn  6205  tfrcllemaccex  6209  dcdifsnid  6351  fnsnsplitdc  6352  funresdfunsndc  6353  eqerlem  6411  qliftfuns  6464  eroveu  6471  cbvixp  6560  mptelixpg  6579  idssen  6622  xpf1o  6688  xpmapen  6694  findcard2d  6735  nnwetri  6754  fiintim  6767  snexxph  6787  fidcenumlemim  6789  fidcenumlemrk  6791  fidcenum  6793  supmoti  6829  isoti  6843  supisoti  6846  cnvti  6855  ordiso2  6869  ctssdccl  6945  finct  6950  ltsopi  7069  addpipqqs  7119  mulpipqqs  7122  archpr  7392  cauappcvgprlemlol  7396  cauappcvgprlemopu  7397  cauappcvgprlemupu  7398  cauappcvgprlemdisj  7400  cauappcvgprlemladdru  7405  cauappcvgprlemladdrl  7406  cauappcvgprlemlim  7410  caucvgprlemlol  7419  caucvgprlemopu  7420  caucvgprlemupu  7421  caucvgprlemdisj  7423  caucvgprlemloc  7424  caucvgprlemcl  7425  caucvgprlemladdrl  7427  caucvgprprlemcbv  7436  caucvgprprlemopu  7448  caucvgprprlemclphr  7454  caucvgprprlemexbt  7455  caucvgsrlembound  7529  caucvgsrlembnd  7536  peano1nnnn  7580  axcaucvglemres  7627  negf1o  8056  lbreu  8606  lbinf  8609  suprubex  8612  suprlubex  8613  suprleubex  8615  1nn  8634  uzind4s  9280  uzind4s2  9281  indstr  9283  supinfneg  9285  infsupneg  9286  eqreznegel  9301  lbzbi  9303  exbtwnzlemex  9913  exbtwnz  9914  rebtwn2zlemstep  9916  rebtwn2z  9918  iseqovex  10115  iseqvalcbv  10116  seqvalcd  10118  seqovcd  10122  seq3f1olemqsum  10159  seq3f1olemp  10161  seq3f1oleml  10162  seq3distr  10172  faclbnd6  10376  fimaxq  10459  cvg1nlemres  10642  resqrexlemsqa  10681  resqrexlemex  10682  cau3lem  10771  fclim  10948  climeu  10950  cn1lem  10968  climcau  11001  climcvg1n  11004  summodclem3  11034  summodclem2a  11035  summodclem2  11036  summodc  11037  zsumdc  11038  fsum3  11041  isumz  11043  isumss2  11047  fsumsersdc  11049  fsum3ser  11051  fsumadd  11060  fsum2dlemstep  11088  fisumcom2  11092  isumshft  11144  cvgratz  11186  mertensabs  11191  odd2np1lem  11410  zsupcl  11481  infssuzex  11483  infssuzledc  11484  bezoutlemmain  11525  bezoutlemeu  11534  gcdmultiple  11547  rplpwr  11554  pw2dvdseu  11684  hashdvds  11735  ennnfonelemg  11754  ennnfoneleminc  11762  ennnfonelemkh  11763  ennnfonelemhf1o  11764  ennnfonelemex  11765  ennnfonelemhom  11766  ennnfonelemrnh  11767  ennnfonelemfun  11768  ennnfonelemdm  11771  ennnfonelemr  11774  ennnfone  11776  inffinp1  11780  ctinf  11781  strsetsid  11828  baspartn  12053  cnpnei  12223  txdis1cn  12282  cnmptid  12285  xmetxp  12489  cncfmptc  12561  cncfmptid  12562  spimd  12652  2spim  12653  ch2var  12654  bj-sbimedh  12658  bj-sbimeh  12659  cbvrald  12674  sumdc2  12685  bdth  12708  bdcdeq  12716  bdne  12730  bdreu  12732  bdcsn  12747  bdsep2  12763  bdsepnft  12764  bdsepnfALT  12766  bdbm1.3ii  12768  bj-nalset  12772  bj-zfpair2  12787  bj-bdfindes  12826  bj-nn0suc0  12827  bj-nntrans  12828  setindft  12842  setindis  12844  bdsetindis  12846  bj-inf2vnlem3  12849  bj-inf2vnlem4  12850  strcoll2  12860  strcollnft  12861  strcollnfALT  12863  sscoll2  12865  nnti  12870  nnsf  12876  peano4nninf  12877  nninfsellemqall  12888  nninfomni  12892  trilpolemeq1  12910