Theorem weq 1503

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

(Instead of introducing weq 1503 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 1503 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  1516  equidqe  1532  ax4sp1  1533  spimfv  1699  chvarfv  1700  equid  1701  nfequid  1702  stdpc6  1703  equcomi  1704  ax6evr  1705  equcom  1706  equcomd  1707  equcoms  1708  equtr  1709  equtrr  1710  equtr2  1711  equequ1  1712  equequ2  1713  ax11i  1714  ax10o  1715  ax10  1717  nfae  1719  hbaes  1720  hbnae  1721  nfnae  1722  hbnaes  1723  equsalh  1726  equsal  1727  dral1  1730  dral2  1731  drex2  1732  drnf1  1733  drnf2  1734  spimth  1735  spimh  1737  spimed  1740  cbv1  1745  cbv1h  1746  cbv1v  1747  cbv2h  1748  cbv2w  1750  cbvalv1  1751  cbvexv1  1752  cbvalh  1753  chvar  1757  sbimi  1764  sb1  1766  sb2  1767  sbequ1  1768  sbequ2  1769  sbequ12  1771  sbequ12r  1772  sbequ12a  1773  sbid  1774  stdpc4  1775  sbh  1776  sb6x  1779  sbequ5  1782  sbequ6  1783  equsb1  1785  equsb2  1786  sbiedh  1787  sbiedv  1789  sbieh  1790  equsalv  1793  equs5a  1794  drsb1  1799  exdistrfor  1800  sb4a  1801  equs45f  1802  sb6f  1803  sb5f  1804  sb4e  1805  hbsb2a  1806  hbsb2e  1807  sbcof2  1810  aev  1812  ax16  1813  dveeq2  1815  dveeq2or  1816  ax11v2  1820  ax11a2  1821  ax11b  1826  equs5  1829  equs5or  1830  sb3  1831  sb4  1832  sb4or  1833  sb4b  1834  sb4bor  1835  hbsb2  1836  nfsb2or  1837  sbequi  1839  sbequ  1840  drsb2  1841  spsbe  1842  spsbim  1843  sbequ8  1847  sbidm  1851  sb5rf  1852  sb6rf  1853  ax16i  1858  spv  1860  speiv  1862  equvin  1863  a16g  1864  a16gb  1865  a16nf  1866  sb56  1885  sb6  1886  sb5  1887  sbnv  1888  sbanv  1889  sborv  1890  sbi1v  1891  sbi2v  1892  cbvalvw  1919  cbvexvw  1920  cbval2  1921  cbvex2  1922  cbvaldva  1928  cbvexdva  1929  cbvex4v  1930  hbs1  1938  hbsbv  1941  nfsbxy  1942  nfsbxyt  1943  nfsbv  1947  equsb3  1951  sbco  1968  sbcocom  1970  sbcomxyyz  1972  sb9v  1978  2sb5  1983  2sb6  1984  sbcom2v  1985  sb6a  1988  2sb5rf  1989  2sb6rf  1990  dfsb7  1991  sb7f  1992  sb7af  1993  sb10f  1995  sbel2x  1998  sbalyz  1999  sbal1yz  2001  sbal1  2002  sbexyz  2003  exsb  2008  2exsb  2009  dvelimALT  2010  dvelimfv  2011  hbsb4t  2013  nfsb4t  2014  dvelimf  2015  dvelimdf  2016  dvelimor  2018  dveeq1  2019  sbal2  2020  euf  2031  eubidh  2032  eubid  2033  hbeu1  2036  nfeu1  2037  sb8eu  2039  nfeuv  2044  sb8euh  2049  eu1  2051  mo2n  2054  euex  2056  eumo0  2057  mo23  2067  mor  2068  modc  2069  eu2  2070  eu3h  2071  mo2r  2078  mo3h  2079  mo2dc  2081  mo4f  2086  eu4  2088  moim  2090  moimv  2092  moanim  2100  mopick  2104  2eu4  2119  euequ1  2121  exists1  2122  elequ1  2152  elequ2  2153  cleljust  2154  elsb1  2155  elsb2  2156  axext3  2160  axext4  2161  bm1.1  2162  eleq1w  2238  cleqh  2277  cbvabw  2300  cbvab  2301  sbab  2305  nfcjust  2307  drnfc1  2336  drnfc2  2337  nfabdw  2338  dvelimdc  2340  dvelimc  2341  nfcvf  2342  cbvralfw  2695  cbvrexfw  2696  cbvralf  2697  cbvrexf  2698  cbvreu  2702  cbvralvw  2708  cbvrexvw  2709  cbvreuvw  2710  cbvraldva2  2711  cbvrexdva2  2712  cbvraldva  2713  cbvrexdva  2714  cbvral2vw  2715  cbvrex2vw  2716  cbvral2v  2717  cbvrex2v  2718  cbvral3v  2719  sbralie  2722  cbvrab  2736  vjust  2739  vex  2741  rr19.3v  2877  rr19.28v  2878  ralab2  2902  rexab2  2904  reu2  2926  reu6  2927  reu3  2928  rmo4  2931  reu4  2932  reu7  2933  reu8  2934  rmo3f  2935  rmo4f  2936  cdeqi  2948  cdeqri  2949  cdeqth  2950  cdeqnot  2951  cdeqal  2952  cdeqab  2953  cdeqim  2956  cdeqcv  2957  cdeqeq  2958  cdeqel  2959  nfccdeq  2961  sbsbc  2967  sbc8g  2971  sbcco2  2986  sbc5  2987  sbcralt  3040  sbcralg  3042  sbcreug  3044  rmo3  3055  cbvcsbw  3062  cbvcsb  3063  csbcow  3069  sbcel12g  3073  sbceqg  3074  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  difjust  3131  unjust  3133  injust  3135  dfss2f  3147  dfdif3  3246  dfnul3  3426  dfif3  3548  preq12bg  3774  eluniab  3822  elintab  3856  int0  3859  dfiunv2  3923  cbviun  3924  cbviin  3925  cbvdisj  3991  disjiun  3999  sndisj  4000  sbcbrg  4058  cbvmptf  4098  cbvmpt  4099  axsep2  4123  bm1.3ii  4125  nalset  4134  zfpow  4176  el  4179  dtruarb  4192  copsexg  4245  opelopabsb  4261  swopo  4307  pofun  4313  issod  4320  frind  4353  zfun  4435  ruv  4550  dtru  4560  dcextest  4581  tfisi  4587  findes  4603  relop  4778  dfdmf  4821  dfrnf  4869  resiexg  4953  dfres2  4960  opabresid  4961  mptresid  4962  imai  4985  issref  5012  intasym  5014  cnvi  5034  rnxpid  5064  cnvpom  5172  nfiota1  5181  cbviota  5184  sb8iota  5186  iotaval  5190  iotanul  5194  iota4  5197  eliota  5205  eliotaeu  5206  csbiotag  5210  dffun2  5227  dffun4  5228  dffun5r  5229  dffun6f  5230  dffun4f  5233  sbcfung  5241  funopg  5251  funinsn  5266  funcnveq  5280  fun11  5284  fununi  5285  funcnvuni  5286  imain  5299  isarep2  5304  brprcneu  5509  fv2  5511  elfv  5514  fv3  5539  relelfvdm  5548  fvmpt2  5600  ralrnmpt  5659  rexrnmpt  5660  ffnfvf  5676  f1veqaeq  5770  dff13f  5771  fliftfuns  5799  canth  5829  cbvriota  5841  csbriotag  5843  acexmid  5874  oprabidlem  5906  cbvmpox  5953  cbvmpo  5954  cbvmpov  5955  mpofun  5977  abrexex2  6125  fmpoco  6217  f1o2ndf1  6229  poxp  6233  tposoprab  6281  tfrlem3-2d  6313  tfrlemi1  6333  tfr1onlemsucfn  6341  tfr1onlemaccex  6349  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemaccex  6362  dcdifsnid  6505  fnsnsplitdc  6506  funresdfunsndc  6507  eqerlem  6566  qliftfuns  6619  eroveu  6626  cbvixp  6715  mptelixpg  6734  idssen  6777  xpf1o  6844  xpmapen  6850  findcard2d  6891  nnwetri  6915  fiintim  6928  snexxph  6949  fidcenumlemim  6951  fidcenumlemrk  6953  fidcenum  6955  supmoti  6992  isoti  7006  supisoti  7009  cnvti  7018  ordiso2  7034  ctssdccl  7110  finct  7115  infnninf  7122  nninfwlpoim  7176  nninfwlpo  7177  exmidontriimlem3  7222  exmidontriimlem4  7223  exmidontriim  7224  onntri13  7237  onntri51  7239  onntri3or  7244  dftap2  7250  netap  7253  2onetap  7254  2omotaplemap  7256  cc1  7264  cc2  7266  ltsopi  7319  addpipqqs  7369  mulpipqqs  7372  archpr  7642  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemupu  7648  cauappcvgprlemdisj  7650  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlemlim  7660  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemupu  7671  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdrl  7677  caucvgprprlemcbv  7686  caucvgprprlemopu  7698  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  suplocexprlemmu  7717  suplocexprlemdisj  7719  caucvgsrlembound  7793  caucvgsrlembnd  7800  suplocsrlem  7807  suplocsr  7808  peano1nnnn  7851  axcaucvglemres  7898  axpre-suploc  7901  negf1o  8339  lbreu  8902  lbinf  8905  suprubex  8908  suprlubex  8909  suprleubex  8911  1nn  8930  uzind4s  9590  uzind4s2  9591  indstr  9593  supinfneg  9595  infsupneg  9596  infregelbex  9598  eqreznegel  9614  lbzbi  9616  elpq  9648  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2z  10255  iseqovex  10456  iseqvalcbv  10457  seqvalcd  10459  seqovcd  10463  seq3f1olemqsum  10500  seq3f1olemp  10502  seq3f1oleml  10503  seq3distr  10513  faclbnd6  10724  fimaxq  10807  cvg1nlemres  10994  resqrexlemsqa  11033  resqrexlemex  11034  cau3lem  11123  fclim  11302  climeu  11304  cn1lem  11322  climcau  11355  climcvg1n  11358  summodclem3  11388  summodclem2a  11389  summodclem2  11390  summodc  11391  zsumdc  11392  fsum3  11395  isumz  11397  isumss2  11401  fsumsersdc  11403  fsum3ser  11405  fsumadd  11414  fsum2dlemstep  11442  fisumcom2  11446  isumshft  11498  cvgratz  11540  mertensabs  11545  prodfdivap  11555  cbvprod  11566  prodmodclem3  11583  prodmodclem2a  11584  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodm1s  11609  fprodp1s  11610  fprod2dlemstep  11630  fprodcom2fi  11634  fprodsplitf  11640  odd2np1lem  11877  zsupcl  11948  infssuzex  11950  infssuzledc  11951  zsupssdc  11955  bezoutlemmain  11999  bezoutlemeu  12008  gcdmultiple  12021  rplpwr  12028  nnwofdc  12039  nnwosdc  12040  isprm5lem  12141  isprm5  12142  pw2dvdseu  12168  hashdvds  12221  eulerthlemh  12231  reumodprminv  12253  pclemub  12287  pclemdc  12288  pceu  12295  pcmptdvds  12343  1arith  12365  4sqlem2  12387  ennnfonelemg  12404  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemrnh  12417  ennnfonelemfun  12418  ennnfonelemdm  12421  ennnfonelemr  12424  ennnfone  12426  inffinp1  12430  ctinf  12431  nninfdclemf  12450  nninfdclemp1  12451  unbendc  12455  infpn2  12457  strsetsid  12495  mgmidmo  12791  lidrididd  12801  mndinvmod  12846  insubm  12872  dfgrp3mlem  12968  mulgaddcom  13007  mulginvcom  13008  isnsg2  13063  srgmulgass  13172  islmodd  13383  lmodvsmmulgdi  13413  rmodislmodlem  13440  rmodislmod  13441  baspartn  13553  cnpnei  13722  txdis1cn  13781  cnmptid  13784  xmetxp  14010  cncfmptc  14085  cncfmptid  14086  dedekindeulemloc  14100  dedekindicclemloc  14109  ivthinclemlr  14118  ivthinclemur  14120  ivthinclemloc  14122  ivthdec  14125  lgseisenlem2  14454  spimd  14520  2spim  14521  ch2var  14522  bj-sbimedh  14526  bj-sbimeh  14527  cbvrald  14543  sumdc2  14554  bdth  14586  bdcdeq  14594  bdne  14608  bdreu  14610  bdcsn  14625  bdsep2  14641  bdsepnft  14642  bdsepnfALT  14644  bdbm1.3ii  14646  bj-nalset  14650  bj-zfpair2  14665  bj-bdfindes  14704  bj-nn0suc0  14705  bj-nntrans  14706  setindft  14720  setindis  14722  bdsetindis  14724  bj-inf2vnlem3  14727  bj-inf2vnlem4  14728  strcoll2  14738  strcollnft  14739  strcollnfALT  14741  sscoll2  14743  nnti  14747  nnsf  14757  peano4nninf  14758  nninfsellemqall  14767  nninfomni  14771  trilpolemeq1  14791  tridceq  14807  redc0  14808  reap0  14809  dceqnconst  14810  dcapnconst  14811  nconstwlpolemgt0  14814