Theorem weq 1501

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

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

Syntax hints:   = wceq 1353

This theorem is referenced by:  alequcoms  1514  equidqe  1530  ax4sp1  1531  spimfv  1697  chvarfv  1698  equid  1699  nfequid  1700  stdpc6  1701  equcomi  1702  ax6evr  1703  equcom  1704  equcomd  1705  equcoms  1706  equtr  1707  equtrr  1708  equtr2  1709  equequ1  1710  equequ2  1711  ax11i  1712  ax10o  1713  ax10  1715  nfae  1717  hbaes  1718  hbnae  1719  nfnae  1720  hbnaes  1721  equsalh  1724  equsal  1725  dral1  1728  dral2  1729  drex2  1730  drnf1  1731  drnf2  1732  spimth  1733  spimh  1735  spimed  1738  cbv1  1743  cbv1h  1744  cbv1v  1745  cbv2h  1746  cbv2w  1748  cbvalv1  1749  cbvexv1  1750  cbvalh  1751  chvar  1755  sbimi  1762  sb1  1764  sb2  1765  sbequ1  1766  sbequ2  1767  sbequ12  1769  sbequ12r  1770  sbequ12a  1771  sbid  1772  stdpc4  1773  sbh  1774  sb6x  1777  sbequ5  1780  sbequ6  1781  equsb1  1783  equsb2  1784  sbiedh  1785  sbiedv  1787  sbieh  1788  equsalv  1791  equs5a  1792  drsb1  1797  exdistrfor  1798  sb4a  1799  equs45f  1800  sb6f  1801  sb5f  1802  sb4e  1803  hbsb2a  1804  hbsb2e  1805  sbcof2  1808  aev  1810  ax16  1811  dveeq2  1813  dveeq2or  1814  ax11v2  1818  ax11a2  1819  ax11b  1824  equs5  1827  equs5or  1828  sb3  1829  sb4  1830  sb4or  1831  sb4b  1832  sb4bor  1833  hbsb2  1834  nfsb2or  1835  sbequi  1837  sbequ  1838  drsb2  1839  spsbe  1840  spsbim  1841  sbequ8  1845  sbidm  1849  sb5rf  1850  sb6rf  1851  ax16i  1856  spv  1858  speiv  1860  equvin  1861  a16g  1862  a16gb  1863  a16nf  1864  sb56  1883  sb6  1884  sb5  1885  sbnv  1886  sbanv  1887  sborv  1888  sbi1v  1889  sbi2v  1890  cbvalvw  1917  cbvexvw  1918  cbval2  1919  cbvex2  1920  cbvaldva  1926  cbvexdva  1927  cbvex4v  1928  hbs1  1936  hbsbv  1939  nfsbxy  1940  nfsbxyt  1941  nfsbv  1945  equsb3  1949  sbco  1966  sbcocom  1968  sbcomxyyz  1970  sb9v  1976  2sb5  1981  2sb6  1982  sbcom2v  1983  sb6a  1986  2sb5rf  1987  2sb6rf  1988  dfsb7  1989  sb7f  1990  sb7af  1991  sb10f  1993  sbel2x  1996  sbalyz  1997  sbal1yz  1999  sbal1  2000  sbexyz  2001  exsb  2006  2exsb  2007  dvelimALT  2008  dvelimfv  2009  hbsb4t  2011  nfsb4t  2012  dvelimf  2013  dvelimdf  2014  dvelimor  2016  dveeq1  2017  sbal2  2018  euf  2029  eubidh  2030  eubid  2031  hbeu1  2034  nfeu1  2035  sb8eu  2037  nfeuv  2042  sb8euh  2047  eu1  2049  mo2n  2052  euex  2054  eumo0  2055  mo23  2065  mor  2066  modc  2067  eu2  2068  eu3h  2069  mo2r  2076  mo3h  2077  mo2dc  2079  mo4f  2084  eu4  2086  moim  2088  moimv  2090  moanim  2098  mopick  2102  2eu4  2117  euequ1  2119  exists1  2120  elequ1  2150  elequ2  2151  cleljust  2152  elsb1  2153  elsb2  2154  axext3  2158  axext4  2159  bm1.1  2160  eleq1w  2236  cleqh  2275  cbvabw  2298  cbvab  2299  sbab  2303  nfcjust  2305  drnfc1  2334  drnfc2  2335  nfabdw  2336  dvelimdc  2338  dvelimc  2339  nfcvf  2340  cbvralfw  2692  cbvrexfw  2693  cbvralf  2694  cbvrexf  2695  cbvreu  2699  cbvralvw  2705  cbvrexvw  2706  cbvreuvw  2707  cbvraldva2  2708  cbvrexdva2  2709  cbvraldva  2710  cbvrexdva  2711  cbvral2vw  2712  cbvrex2vw  2713  cbvral2v  2714  cbvrex2v  2715  cbvral3v  2716  sbralie  2719  cbvrab  2733  vjust  2736  vex  2738  rr19.3v  2874  rr19.28v  2875  ralab2  2899  rexab2  2901  reu2  2923  reu6  2924  reu3  2925  rmo4  2928  reu4  2929  reu7  2930  reu8  2931  rmo3f  2932  rmo4f  2933  cdeqi  2945  cdeqri  2946  cdeqth  2947  cdeqnot  2948  cdeqal  2949  cdeqab  2950  cdeqim  2953  cdeqcv  2954  cdeqeq  2955  cdeqel  2956  nfccdeq  2958  sbsbc  2964  sbc8g  2968  sbcco2  2983  sbc5  2984  sbcralt  3037  sbcralg  3039  sbcreug  3041  rmo3  3052  cbvcsbw  3059  cbvcsb  3060  csbcow  3066  sbcel12g  3070  sbceqg  3071  cbvralcsf  3117  cbvrexcsf  3118  cbvreucsf  3119  cbvrabcsf  3120  difjust  3128  unjust  3130  injust  3132  dfss2f  3144  dfdif3  3243  dfnul3  3423  dfif3  3545  preq12bg  3769  eluniab  3817  elintab  3851  int0  3854  dfiunv2  3918  cbviun  3919  cbviin  3920  cbvdisj  3985  disjiun  3993  sndisj  3994  sbcbrg  4052  cbvmptf  4092  cbvmpt  4093  axsep2  4117  bm1.3ii  4119  nalset  4128  zfpow  4170  el  4173  dtruarb  4186  copsexg  4238  opelopabsb  4254  swopo  4300  pofun  4306  issod  4313  frind  4346  zfun  4428  ruv  4543  dtru  4553  dcextest  4574  tfisi  4580  findes  4596  relop  4770  dfdmf  4813  dfrnf  4861  resiexg  4945  dfres2  4952  opabresid  4953  mptresid  4954  imai  4977  issref  5003  intasym  5005  cnvi  5025  rnxpid  5055  cnvpom  5163  nfiota1  5172  cbviota  5175  sb8iota  5177  iotaval  5181  iotanul  5185  iota4  5188  eliota  5196  eliotaeu  5197  csbiotag  5201  dffun2  5218  dffun4  5219  dffun5r  5220  dffun6f  5221  dffun4f  5224  sbcfung  5232  funopg  5242  funinsn  5257  funcnveq  5271  fun11  5275  fununi  5276  funcnvuni  5277  imain  5290  isarep2  5295  brprcneu  5500  fv2  5502  elfv  5505  fv3  5530  relelfvdm  5539  fvmpt2  5591  ralrnmpt  5650  rexrnmpt  5651  ffnfvf  5667  f1veqaeq  5760  dff13f  5761  fliftfuns  5789  canth  5819  cbvriota  5831  csbriotag  5833  acexmid  5864  oprabidlem  5896  cbvmpox  5943  cbvmpo  5944  cbvmpov  5945  mpofun  5967  abrexex2  6115  fmpoco  6207  f1o2ndf1  6219  poxp  6223  tposoprab  6271  tfrlem3-2d  6303  tfrlemi1  6323  tfr1onlemsucfn  6331  tfr1onlemaccex  6339  tfrcllemsucfn  6344  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllembfn  6348  tfrcllemaccex  6352  dcdifsnid  6495  fnsnsplitdc  6496  funresdfunsndc  6497  eqerlem  6556  qliftfuns  6609  eroveu  6616  cbvixp  6705  mptelixpg  6724  idssen  6767  xpf1o  6834  xpmapen  6840  findcard2d  6881  nnwetri  6905  fiintim  6918  snexxph  6939  fidcenumlemim  6941  fidcenumlemrk  6943  fidcenum  6945  supmoti  6982  isoti  6996  supisoti  6999  cnvti  7008  ordiso2  7024  ctssdccl  7100  finct  7105  infnninf  7112  nninfwlpoim  7166  nninfwlpo  7167  exmidontriimlem3  7212  exmidontriimlem4  7213  exmidontriim  7214  onntri13  7227  onntri51  7229  onntri3or  7234  cc1  7239  cc2  7241  ltsopi  7294  addpipqqs  7344  mulpipqqs  7347  archpr  7617  cauappcvgprlemlol  7621  cauappcvgprlemopu  7622  cauappcvgprlemupu  7623  cauappcvgprlemdisj  7625  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  cauappcvgprlemlim  7635  caucvgprlemlol  7644  caucvgprlemopu  7645  caucvgprlemupu  7646  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprlemcl  7650  caucvgprlemladdrl  7652  caucvgprprlemcbv  7661  caucvgprprlemopu  7673  caucvgprprlemclphr  7679  caucvgprprlemexbt  7680  suplocexprlemmu  7692  suplocexprlemdisj  7694  caucvgsrlembound  7768  caucvgsrlembnd  7775  suplocsrlem  7782  suplocsr  7783  peano1nnnn  7826  axcaucvglemres  7873  axpre-suploc  7876  negf1o  8313  lbreu  8875  lbinf  8878  suprubex  8881  suprlubex  8882  suprleubex  8884  1nn  8903  uzind4s  9563  uzind4s2  9564  indstr  9566  supinfneg  9568  infsupneg  9569  infregelbex  9571  eqreznegel  9587  lbzbi  9589  elpq  9621  exbtwnzlemex  10220  exbtwnz  10221  rebtwn2zlemstep  10223  rebtwn2z  10225  iseqovex  10426  iseqvalcbv  10427  seqvalcd  10429  seqovcd  10433  seq3f1olemqsum  10470  seq3f1olemp  10472  seq3f1oleml  10473  seq3distr  10483  faclbnd6  10692  fimaxq  10775  cvg1nlemres  10962  resqrexlemsqa  11001  resqrexlemex  11002  cau3lem  11091  fclim  11270  climeu  11272  cn1lem  11290  climcau  11323  climcvg1n  11326  summodclem3  11356  summodclem2a  11357  summodclem2  11358  summodc  11359  zsumdc  11360  fsum3  11363  isumz  11365  isumss2  11369  fsumsersdc  11371  fsum3ser  11373  fsumadd  11382  fsum2dlemstep  11410  fisumcom2  11414  isumshft  11466  cvgratz  11508  mertensabs  11513  prodfdivap  11523  cbvprod  11534  prodmodclem3  11551  prodmodclem2a  11552  prodmodclem2  11553  prodmodc  11554  zproddc  11555  fprodseq  11559  fprodm1s  11577  fprodp1s  11578  fprod2dlemstep  11598  fprodcom2fi  11602  fprodsplitf  11608  odd2np1lem  11844  zsupcl  11915  infssuzex  11917  infssuzledc  11918  zsupssdc  11922  bezoutlemmain  11966  bezoutlemeu  11975  gcdmultiple  11988  rplpwr  11995  nnwofdc  12006  nnwosdc  12007  isprm5lem  12108  isprm5  12109  pw2dvdseu  12135  hashdvds  12188  eulerthlemh  12198  reumodprminv  12220  pclemub  12254  pclemdc  12255  pceu  12262  pcmptdvds  12310  1arith  12332  4sqlem2  12354  ennnfonelemg  12371  ennnfoneleminc  12379  ennnfonelemkh  12380  ennnfonelemhf1o  12381  ennnfonelemex  12382  ennnfonelemhom  12383  ennnfonelemrnh  12384  ennnfonelemfun  12385  ennnfonelemdm  12388  ennnfonelemr  12391  ennnfone  12393  inffinp1  12397  ctinf  12398  nninfdclemf  12417  nninfdclemp1  12418  unbendc  12422  infpn2  12424  strsetsid  12462  mgmidmo  12657  lidrididd  12667  mndinvmod  12709  insubm  12734  dfgrp3mlem  12829  mulgaddcom  12867  mulginvcom  12868  srgmulgass  12969  baspartn  13119  cnpnei  13290  txdis1cn  13349  cnmptid  13352  xmetxp  13578  cncfmptc  13653  cncfmptid  13654  dedekindeulemloc  13668  dedekindicclemloc  13677  ivthinclemlr  13686  ivthinclemur  13688  ivthinclemloc  13690  ivthdec  13693  spimd  14077  2spim  14078  ch2var  14079  bj-sbimedh  14083  bj-sbimeh  14084  cbvrald  14100  sumdc2  14111  bdth  14143  bdcdeq  14151  bdne  14165  bdreu  14167  bdcsn  14182  bdsep2  14198  bdsepnft  14199  bdsepnfALT  14201  bdbm1.3ii  14203  bj-nalset  14207  bj-zfpair2  14222  bj-bdfindes  14261  bj-nn0suc0  14262  bj-nntrans  14263  setindft  14277  setindis  14279  bdsetindis  14281  bj-inf2vnlem3  14284  bj-inf2vnlem4  14285  strcoll2  14295  strcollnft  14296  strcollnfALT  14298  sscoll2  14300  nnti  14304  nnsf  14315  peano4nninf  14316  nninfsellemqall  14325  nninfomni  14329  trilpolemeq1  14349  tridceq  14365  redc0  14366  reap0  14367  dceqnconst  14368  dcapnconst  14369  nconstwlpolemgt0  14372