Theorem weq 1435

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

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

Syntax hints:   = wceq 1287

This theorem is referenced by:  alequcoms  1452  equidqe  1468  ax4sp1  1469  equid  1632  nfequid  1633  stdpc6  1634  equcomi  1635  ax6evr  1636  equcom  1637  equcoms  1638  equtr  1639  equtrr  1640  equtr2  1641  equequ1  1642  equequ2  1643  elequ1  1644  elequ2  1645  ax11i  1646  ax10o  1647  ax10  1649  nfae  1651  hbaes  1652  hbnae  1653  nfnae  1654  hbnaes  1655  equsalh  1658  equsal  1659  dral1  1662  dral2  1663  drex2  1664  drnf1  1665  drnf2  1666  spimth  1667  spimh  1669  spimed  1672  cbv1  1676  cbv1h  1677  cbv2h  1678  cbvalh  1680  chvar  1684  sbimi  1691  sb1  1693  sb2  1694  sbequ1  1695  sbequ2  1696  sbequ12  1698  sbequ12r  1699  sbequ12a  1700  sbid  1701  stdpc4  1702  sbh  1703  sb6x  1706  sbequ5  1709  sbequ6  1710  equsb1  1712  equsb2  1713  sbiedh  1714  sbiedv  1716  sbieh  1717  equs5a  1719  drsb1  1724  exdistrfor  1725  sb4a  1726  equs45f  1727  sb6f  1728  sb5f  1729  sb4e  1730  hbsb2a  1731  hbsb2e  1732  sbcof2  1735  aev  1737  ax16  1738  dveeq2  1740  dveeq2or  1741  ax11v2  1745  ax11a2  1746  ax11b  1751  equs5  1754  equs5or  1755  sb3  1756  sb4  1757  sb4or  1758  sb4b  1759  sb4bor  1760  hbsb2  1761  nfsb2or  1762  sbequi  1764  sbequ  1765  drsb2  1766  spsbe  1767  spsbim  1768  sbequ8  1772  sbidm  1776  sb5rf  1777  sb6rf  1778  ax16i  1783  spv  1785  speiv  1787  equvin  1788  a16g  1789  a16gb  1790  a16nf  1791  sb56  1810  sb6  1811  sb5  1812  sbnv  1813  sbanv  1814  sborv  1815  sbi1v  1816  sbi2v  1817  cbval2  1841  cbvex2  1842  cbvaldva  1848  cbvexdva  1849  cbvex4v  1850  cleljust  1858  hbs1  1859  hbsbv  1862  nfsbxy  1863  nfsbxyt  1864  equsb3  1870  sbco  1887  sbcocom  1889  sbcomxyyz  1891  elsb3  1897  elsb4  1898  sb9v  1899  2sb5  1904  2sb6  1905  sbcom2v  1906  sb6a  1909  2sb5rf  1910  2sb6rf  1911  dfsb7  1912  sb7f  1913  sb7af  1914  sb10f  1916  sbel2x  1919  sbalyz  1920  sbal1yz  1922  sbal1  1923  sbexyz  1924  exsb  1929  2exsb  1930  dvelimALT  1931  dvelimfv  1932  hbsb4t  1934  nfsb4t  1935  dvelimf  1936  dvelimdf  1937  dvelimor  1939  dveeq1  1940  sbal2  1943  euf  1950  eubidh  1951  eubid  1952  hbeu1  1955  nfeu1  1956  sb8eu  1958  nfeuv  1963  sb8euh  1968  eu1  1970  mo2n  1973  euex  1975  eumo0  1976  mo23  1986  mor  1987  modc  1988  eu2  1989  eu3h  1990  mo2r  1997  mo3h  1998  mo2dc  2000  mo4f  2005  eu4  2007  moim  2009  moimv  2011  moanim  2019  mopick  2023  2eu4  2038  euequ1  2040  exists1  2041  axext3  2068  axext4  2069  bm1.1  2070  eleq1w  2145  cleqh  2184  cbvab  2207  sbab  2211  nfcjust  2213  drnfc1  2241  drnfc2  2242  dvelimdc  2244  dvelimc  2245  nfcvf  2246  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvraldva2  2590  cbvrexdva2  2591  cbvraldva  2592  cbvrexdva  2593  cbvral2v  2594  cbvrex2v  2595  cbvral3v  2596  cbvrab  2613  vjust  2616  vex  2618  rr19.3v  2746  rr19.28v  2747  ralab2  2770  rexab2  2772  reu2  2794  reu6  2795  reu3  2796  rmo4  2799  reu4  2800  reu7  2801  reu8  2802  cdeqi  2814  cdeqri  2815  cdeqth  2816  cdeqnot  2817  cdeqal  2818  cdeqab  2819  cdeqim  2822  cdeqcv  2823  cdeqeq  2824  cdeqel  2825  nfccdeq  2827  sbsbc  2833  sbc8g  2836  sbcco2  2851  sbc5  2852  sbcralt  2904  sbcralg  2906  sbcreug  2908  rmo3  2919  cbvcsb  2926  sbcel12g  2935  sbceqg  2936  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  difjust  2989  unjust  2991  injust  2993  dfss2f  3005  dfdif3  3099  dfnul3  3278  dfif3  3392  preq12bg  3600  eluniab  3648  elintab  3682  int0  3685  dfiunv2  3749  cbviun  3750  cbviin  3751  cbvdisj  3811  sndisj  3816  sbcbrg  3869  cbvmptf  3907  cbvmpt  3908  axsep2  3933  bm1.3ii  3935  nalset  3944  zfpow  3985  el  3988  dtruarb  4000  copsexg  4045  opelopabsb  4061  swopo  4107  pofun  4113  issod  4120  frind  4153  zfun  4235  ruv  4339  dtru  4349  dcextest  4369  tfisi  4375  findes  4391  relop  4554  dfdmf  4597  dfrnf  4644  resiexg  4724  dfres2  4731  opabresid  4732  mptresid  4733  imai  4755  issref  4781  intasym  4783  cnvi  4802  rnxpid  4831  cnvpom  4939  nfiota1  4948  cbviota  4951  sb8iota  4953  iotaval  4957  iotanul  4961  iota4  4964  csbiotag  4974  dffun2  4991  dffun4  4992  dffun5r  4993  dffun6f  4994  dffun4f  4997  sbcfung  5004  funopg  5013  funinsn  5028  funcnveq  5042  fun11  5046  fununi  5047  funcnvuni  5048  imain  5061  isarep2  5066  brprcneu  5261  fv2  5263  elfv  5266  fv3  5291  relelfvdm  5299  fvmpt2  5349  ralrnmpt  5404  rexrnmpt  5405  ffnfvf  5420  f1veqaeq  5509  dff13f  5510  fliftfuns  5538  cbvriota  5579  csbriotag  5581  acexmid  5612  oprabidlem  5637  cbvmpt2x  5683  cbvmpt2  5684  cbvmpt2v  5685  mpt2fun  5704  abrexex2  5852  fmpt2co  5938  f1o2ndf1  5950  poxp  5954  tposoprab  5999  tfrlem3-2d  6031  tfrlemi1  6051  tfr1onlemsucfn  6059  tfr1onlemaccex  6067  tfrcllemsucfn  6072  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemaccex  6080  dcdifsnid  6217  eqerlem  6275  qliftfuns  6328  eroveu  6335  idssen  6446  xpf1o  6512  xpmapen  6518  findcard2d  6559  nnwetri  6578  snexxph  6608  supmoti  6632  isoti  6646  supisoti  6649  cnvti  6658  ordiso2  6672  djuss  6705  ltsopi  6823  addpipqqs  6873  mulpipqqs  6876  archpr  7146  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemupu  7152  cauappcvgprlemdisj  7154  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlemlim  7164  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemupu  7175  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdrl  7181  caucvgprprlemcbv  7190  caucvgprprlemopu  7202  caucvgprprlemclphr  7208  caucvgprprlemexbt  7209  caucvgsrlembound  7283  caucvgsrlembnd  7290  peano1nnnn  7333  axcaucvglemres  7378  negf1o  7804  lbreu  8341  lbinf  8344  suprubex  8347  suprlubex  8348  suprleubex  8350  1nn  8368  uzind4s  9010  uzind4s2  9011  indstr  9013  supinfneg  9015  infsupneg  9016  eqreznegel  9031  lbzbi  9033  exbtwnzlemex  9589  exbtwnz  9590  rebtwn2zlemstep  9592  rebtwn2z  9594  iseqovex  9787  iseqvalcbv  9789  iseqf1olemqsum  9834  iseqf1olemp  9836  iseqdistr  9847  faclbnd6  10049  fimaxq  10132  cvg1nlemres  10314  resqrexlemsqa  10353  resqrexlemex  10354  cau3lem  10443  fclim  10577  climeu  10579  cn1lem  10596  climcau  10628  climcvg1n  10631  isummolem3  10661  isummolem2a  10662  isummolem2  10663  isummo  10664  zisum  10665  fisum  10667  isumz  10669  isumss2  10673  fisumsers  10675  odd2np1lem  10754  zsupcl  10825  infssuzex  10827  infssuzledc  10828  bezoutlemmain  10869  bezoutlemeu  10878  gcdmultiple  10891  rplpwr  10898  pw2dvdseu  11028  hashdvds  11079  spimd  11111  2spim  11112  ch2var  11113  bj-sbimedh  11117  bj-sbimeh  11118  cbvrald  11133  sumdc2  11144  bdth  11167  bdcdeq  11175  bdne  11189  bdreu  11191  bdcsn  11206  bdsep2  11222  bdsepnft  11223  bdsepnfALT  11225  bdbm1.3ii  11227  bj-nalset  11231  bj-zfpair2  11246  bj-bdfindes  11289  bj-nn0suc0  11290  bj-nntrans  11291  setindft  11305  setindis  11307  bdsetindis  11309  bj-inf2vnlem3  11312  bj-inf2vnlem4  11313  strcoll2  11323  strcollnft  11324  strcollnfALT  11326  sscoll2  11328  nnti  11337  nnsf  11340  peano4nninf  11341  nninfsellemqall  11352  nninfomni  11356