Theorem weq 1432

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

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

Syntax hints:   = wceq 1284

This theorem is referenced by:  alequcoms  1449  equidqe  1465  ax4sp1  1466  equid  1629  nfequid  1630  stdpc6  1631  equcomi  1632  equcom  1633  equcoms  1634  equtr  1635  equtrr  1636  equtr2  1637  equequ1  1638  equequ2  1639  elequ1  1640  elequ2  1641  ax11i  1642  ax10o  1643  ax10  1645  nfae  1647  hbaes  1648  hbnae  1649  nfnae  1650  hbnaes  1651  equsalh  1654  equsal  1655  dral1  1658  dral2  1659  drex2  1660  drnf1  1661  drnf2  1662  spimth  1663  spimh  1665  spimed  1668  cbv1  1672  cbv1h  1673  cbv2h  1674  cbvalh  1676  chvar  1680  sbimi  1687  sb1  1689  sb2  1690  sbequ1  1691  sbequ2  1692  sbequ12  1694  sbequ12r  1695  sbequ12a  1696  sbid  1697  stdpc4  1698  sbh  1699  sb6x  1702  sbequ5  1705  sbequ6  1706  equsb1  1708  equsb2  1709  sbiedh  1710  sbiedv  1712  sbieh  1713  equs5a  1715  drsb1  1720  exdistrfor  1721  sb4a  1722  equs45f  1723  sb6f  1724  sb5f  1725  sb4e  1726  hbsb2a  1727  hbsb2e  1728  sbcof2  1731  aev  1733  ax16  1734  dveeq2  1736  dveeq2or  1737  ax11v2  1741  ax11a2  1742  ax11b  1747  equs5  1750  equs5or  1751  sb3  1752  sb4  1753  sb4or  1754  sb4b  1755  sb4bor  1756  hbsb2  1757  nfsb2or  1758  sbequi  1760  sbequ  1761  drsb2  1762  spsbe  1763  spsbim  1764  sbequ8  1768  sbidm  1772  sb5rf  1773  sb6rf  1774  ax16i  1779  spv  1781  speiv  1783  equvin  1784  a16g  1785  a16gb  1786  a16nf  1787  sb56  1806  sb6  1807  sb5  1808  sbnv  1809  sbanv  1810  sborv  1811  sbi1v  1812  sbi2v  1813  cbval2  1837  cbvex2  1838  cbvaldva  1844  cbvexdva  1845  cbvex4v  1846  cleljust  1854  hbs1  1855  hbsbv  1858  nfsbxy  1859  nfsbxyt  1860  equsb3  1866  sbco  1883  sbcocom  1885  sbcomxyyz  1887  elsb3  1893  elsb4  1894  sb9v  1895  2sb5  1900  2sb6  1901  sbcom2v  1902  sb6a  1905  2sb5rf  1906  2sb6rf  1907  dfsb7  1908  sb7f  1909  sb7af  1910  sb10f  1912  sbel2x  1915  sbalyz  1916  sbal1yz  1918  sbal1  1919  sbexyz  1920  exsb  1925  2exsb  1926  dvelimALT  1927  dvelimfv  1928  hbsb4t  1930  nfsb4t  1931  dvelimf  1932  dvelimdf  1933  dvelimor  1935  dveeq1  1936  sbal2  1939  euf  1946  eubidh  1947  eubid  1948  hbeu1  1951  nfeu1  1952  sb8eu  1954  nfeuv  1959  sb8euh  1964  eu1  1966  mo2n  1969  euex  1971  eumo0  1972  mo23  1982  mor  1983  modc  1984  eu2  1985  eu3h  1986  mo2r  1993  mo3h  1994  mo2dc  1996  mo4f  2001  eu4  2003  moim  2005  moimv  2007  moanim  2015  mopick  2019  2eu4  2034  euequ1  2036  exists1  2037  axext3  2064  axext4  2065  bm1.1  2066  cleqh  2178  cbvab  2201  sbab  2205  nfcjust  2207  drnfc1  2235  drnfc2  2236  dvelimdc  2238  dvelimc  2239  nfcvf  2240  cbvralf  2571  cbvrexf  2572  cbvreu  2575  cbvraldva2  2581  cbvrexdva2  2582  cbvraldva  2583  cbvrexdva  2584  cbvral2v  2585  cbvrex2v  2586  cbvral3v  2587  cbvrab  2599  vjust  2602  vex  2604  rr19.3v  2733  rr19.28v  2734  ralab2  2756  rexab2  2758  reu2  2780  reu6  2781  reu3  2782  rmo4  2785  reu4  2786  reu7  2787  reu8  2788  cdeqi  2800  cdeqri  2801  cdeqth  2802  cdeqnot  2803  cdeqal  2804  cdeqab  2805  cdeqim  2808  cdeqcv  2809  cdeqeq  2810  cdeqel  2811  nfccdeq  2813  sbsbc  2819  sbc8g  2822  sbcco2  2837  sbc5  2838  sbcralt  2890  sbcralg  2892  sbcreug  2894  rmo3  2905  cbvcsb  2912  sbcel12g  2921  sbceqg  2922  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  difjust  2974  unjust  2976  injust  2978  dfss2f  2990  dfnul3  3254  dfif3  3364  preq12bg  3565  eluniab  3613  elintab  3647  int0  3650  dfiunv2  3714  cbviun  3715  cbviin  3716  cbvdisj  3776  sndisj  3781  sbcbrg  3834  cbvmpt  3872  axsep2  3897  bm1.3ii  3899  nalset  3908  zfpow  3949  el  3952  dtruarb  3962  copsexg  3999  opelopabsb  4015  swopo  4061  pofun  4067  issod  4074  frind  4107  zfun  4189  ruv  4293  dtru  4303  tfisi  4328  findes  4344  relop  4504  dfdmf  4546  dfrnf  4593  resiexg  4673  dfres2  4678  opabresid  4679  mptresid  4680  imai  4701  issref  4727  intasym  4729  cnvi  4748  rnxpid  4775  cnvpom  4880  nfiota1  4889  cbviota  4892  sb8iota  4894  iotaval  4898  iotanul  4902  iota4  4905  csbiotag  4915  dffun2  4932  dffun4  4933  dffun5r  4934  dffun6f  4935  dffun4f  4938  sbcfung  4945  funopg  4954  funcnveq  4982  fun11  4986  fununi  4987  funcnvuni  4988  imain  5001  isarep2  5006  brprcneu  5191  fv2  5193  elfv  5196  fv3  5218  relelfvdm  5226  fvmpt2  5275  ralrnmpt  5330  rexrnmpt  5331  ffnfvf  5345  f1veqaeq  5429  dff13f  5430  fliftfuns  5458  cbvriota  5498  csbriotag  5500  acexmid  5531  oprabidlem  5556  cbvmpt2x  5602  cbvmpt2  5603  cbvmpt2v  5604  mpt2fun  5623  abrexex2  5771  fmpt2co  5857  f1o2ndf1  5869  poxp  5873  tposoprab  5918  tfrlem3-2d  5951  tfrlemi1  5969  eqerlem  6160  qliftfuns  6213  eroveu  6220  idssen  6280  findcard2d  6375  nnwetri  6382  supmoti  6406  isoti  6420  supisoti  6423  cnvti  6432  ordiso2  6446  ltsopi  6510  addpipqqs  6560  mulpipqqs  6563  archpr  6833  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemupu  6839  cauappcvgprlemdisj  6841  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlemlim  6851  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemupu  6862  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdrl  6868  caucvgprprlemcbv  6877  caucvgprprlemopu  6889  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgsrlembound  6970  caucvgsrlembnd  6977  peano1nnnn  7020  axcaucvglemres  7065  negf1o  7486  lbreu  8023  lbinf  8026  suprubex  8029  suprlubex  8030  suprleubex  8032  1nn  8050  uzind4s  8678  uzind4s2  8679  indstr  8681  supinfneg  8683  infsupneg  8684  eqreznegel  8699  lbzbi  8701  qbtwnzlemstep  9257  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  iseqovex  9439  iseqcaopr3  9460  iseqdistr  9470  faclbnd6  9671  cvg1nlemres  9871  resqrexlemsqa  9910  resqrexlemex  9911  cau3lem  10000  fclim  10133  climeu  10135  cn1lem  10152  climcau  10184  climcvg1n  10187  odd2np1lem  10271  zsupcl  10343  infssuzex  10345  infssuzledc  10346  bezoutlemmain  10387  bezoutlemeu  10396  gcdmultiple  10409  rplpwr  10416  pw2dvdseu  10546  spimd  10576  2spim  10577  ch2var  10578  bj-sbimedh  10582  bj-sbimeh  10583  cbvrald  10598  bdth  10622  bdcdeq  10630  bdne  10644  bdreu  10646  bdcsn  10661  bdsep2  10677  bdsepnft  10678  bdsepnfALT  10680  bdbm1.3ii  10682  bj-nalset  10686  bj-zfpair2  10701  bj-bdfindes  10744  bj-nn0suc0  10745  bj-nntrans  10746  setindft  10760  setindis  10762  bdsetindis  10764  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768  strcoll2  10778  strcollnft  10779  strcollnfALT  10781  sscoll2  10783