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 x = y

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1353	1 wff x = y

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  2703  cbvralvw  2709  cbvrexvw  2710  cbvreuvw  2711  cbvraldva2  2712  cbvrexdva2  2713  cbvraldva  2714  cbvrexdva  2715  cbvral2vw  2716  cbvrex2vw  2717  cbvral2v  2718  cbvrex2v  2719  cbvral3v  2720  sbralie  2723  cbvrab  2737  vjust  2740  vex  2742  rr19.3v  2878  rr19.28v  2879  ralab2  2903  rexab2  2905  reu2  2927  reu6  2928  reu3  2929  rmo4  2932  reu4  2933  reu7  2934  reu8  2935  rmo3f  2936  rmo4f  2937  cdeqi  2949  cdeqri  2950  cdeqth  2951  cdeqnot  2952  cdeqal  2953  cdeqab  2954  cdeqim  2957  cdeqcv  2958  cdeqeq  2959  cdeqel  2960  nfccdeq  2962  sbsbc  2968  sbc8g  2972  sbcco2  2987  sbc5  2988  sbcralt  3041  sbcralg  3043  sbcreug  3045  rmo3  3056  cbvcsbw  3063  cbvcsb  3064  csbcow  3070  sbcel12g  3074  sbceqg  3075  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  difjust  3132  unjust  3134  injust  3136  dfss2f  3148  dfdif3  3247  dfnul3  3427  dfif3  3549  preq12bg  3775  eluniab  3823  elintab  3857  int0  3860  dfiunv2  3924  cbviun  3925  cbviin  3926  cbvdisj  3992  disjiun  4000  sndisj  4001  sbcbrg  4059  cbvmptf  4099  cbvmpt  4100  axsep2  4124  bm1.3ii  4126  nalset  4135  zfpow  4177  el  4180  dtruarb  4193  copsexg  4246  opelopabsb  4262  swopo  4308  pofun  4314  issod  4321  frind  4354  zfun  4436  ruv  4551  dtru  4561  dcextest  4582  tfisi  4588  findes  4604  relop  4779  dfdmf  4822  dfrnf  4870  resiexg  4954  dfres2  4961  opabresid  4962  mptresid  4963  imai  4986  issref  5013  intasym  5015  cnvi  5035  rnxpid  5065  cnvpom  5173  nfiota1  5182  cbviota  5185  sb8iota  5187  iotaval  5191  iotanul  5195  iota4  5198  eliota  5206  eliotaeu  5207  csbiotag  5211  dffun2  5228  dffun4  5229  dffun5r  5230  dffun6f  5231  dffun4f  5234  sbcfung  5242  funopg  5252  funinsn  5267  funcnveq  5281  fun11  5285  fununi  5286  funcnvuni  5287  imain  5300  isarep2  5305  brprcneu  5510  fv2  5512  elfv  5515  fv3  5540  relelfvdm  5549  fvmpt2  5601  ralrnmpt  5660  rexrnmpt  5661  ffnfvf  5677  f1veqaeq  5772  dff13f  5773  fliftfuns  5801  canth  5831  cbvriota  5843  csbriotag  5845  acexmid  5876  oprabidlem  5908  cbvmpox  5955  cbvmpo  5956  cbvmpov  5957  mpofun  5979  abrexex2  6127  fmpoco  6219  f1o2ndf1  6231  poxp  6235  tposoprab  6283  tfrlem3-2d  6315  tfrlemi1  6335  tfr1onlemsucfn  6343  tfr1onlemaccex  6351  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  dcdifsnid  6507  fnsnsplitdc  6508  funresdfunsndc  6509  eqerlem  6568  qliftfuns  6621  eroveu  6628  cbvixp  6717  mptelixpg  6736  idssen  6779  xpf1o  6846  xpmapen  6852  findcard2d  6893  nnwetri  6917  fiintim  6930  snexxph  6951  fidcenumlemim  6953  fidcenumlemrk  6955  fidcenum  6957  supmoti  6994  isoti  7008  supisoti  7011  cnvti  7020  ordiso2  7036  ctssdccl  7112  finct  7117  infnninf  7124  nninfwlpoim  7178  nninfwlpo  7179  exmidontriimlem3  7224  exmidontriimlem4  7225  exmidontriim  7226  onntri13  7239  onntri51  7241  onntri3or  7246  dftap2  7252  netap  7255  2onetap  7256  2omotaplemap  7258  cc1  7266  cc2  7268  ltsopi  7321  addpipqqs  7371  mulpipqqs  7374  archpr  7644  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlemlim  7662  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdrl  7679  caucvgprprlemcbv  7688  caucvgprprlemopu  7700  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  suplocexprlemmu  7719  suplocexprlemdisj  7721  caucvgsrlembound  7795  caucvgsrlembnd  7802  suplocsrlem  7809  suplocsr  7810  peano1nnnn  7853  axcaucvglemres  7900  axpre-suploc  7903  negf1o  8341  lbreu  8904  lbinf  8907  suprubex  8910  suprlubex  8911  suprleubex  8913  1nn  8932  uzind4s  9592  uzind4s2  9593  indstr  9595  supinfneg  9597  infsupneg  9598  infregelbex  9600  eqreznegel  9616  lbzbi  9618  elpq  9650  exbtwnzlemex  10252  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2z  10257  iseqovex  10458  iseqvalcbv  10459  seqvalcd  10461  seqovcd  10465  seq3f1olemqsum  10502  seq3f1olemp  10504  seq3f1oleml  10505  seq3distr  10515  faclbnd6  10726  fimaxq  10809  cvg1nlemres  10996  resqrexlemsqa  11035  resqrexlemex  11036  cau3lem  11125  fclim  11304  climeu  11306  cn1lem  11324  climcau  11357  climcvg1n  11360  summodclem3  11390  summodclem2a  11391  summodclem2  11392  summodc  11393  zsumdc  11394  fsum3  11397  isumz  11399  isumss2  11403  fsumsersdc  11405  fsum3ser  11407  fsumadd  11416  fsum2dlemstep  11444  fisumcom2  11448  isumshft  11500  cvgratz  11542  mertensabs  11547  prodfdivap  11557  cbvprod  11568  prodmodclem3  11585  prodmodclem2a  11586  prodmodclem2  11587  prodmodc  11588  zproddc  11589  fprodseq  11593  fprodm1s  11611  fprodp1s  11612  fprod2dlemstep  11632  fprodcom2fi  11636  fprodsplitf  11642  odd2np1lem  11879  zsupcl  11950  infssuzex  11952  infssuzledc  11953  zsupssdc  11957  bezoutlemmain  12001  bezoutlemeu  12010  gcdmultiple  12023  rplpwr  12030  nnwofdc  12041  nnwosdc  12042  isprm5lem  12143  isprm5  12144  pw2dvdseu  12170  hashdvds  12223  eulerthlemh  12233  reumodprminv  12255  pclemub  12289  pclemdc  12290  pceu  12297  pcmptdvds  12345  1arith  12367  4sqlem2  12389  ennnfonelemg  12406  ennnfoneleminc  12414  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemrnh  12419  ennnfonelemfun  12420  ennnfonelemdm  12423  ennnfonelemr  12426  ennnfone  12428  inffinp1  12432  ctinf  12433  nninfdclemf  12452  nninfdclemp1  12453  unbendc  12457  infpn2  12459  strsetsid  12497  mgmidmo  12796  lidrididd  12806  mndinvmod  12851  insubm  12877  dfgrp3mlem  12973  mulgaddcom  13012  mulginvcom  13013  isnsg2  13068  srgmulgass  13177  islmodd  13388  lmodvsmmulgdi  13418  rmodislmodlem  13445  rmodislmod  13446  lssats2  13505  baspartn  13635  cnpnei  13804  txdis1cn  13863  cnmptid  13866  xmetxp  14092  cncfmptc  14167  cncfmptid  14168  dedekindeulemloc  14182  dedekindicclemloc  14191  ivthinclemlr  14200  ivthinclemur  14202  ivthinclemloc  14204  ivthdec  14207  lgseisenlem2  14536  spimd  14602  2spim  14603  ch2var  14604  bj-sbimedh  14608  bj-sbimeh  14609  cbvrald  14625  sumdc2  14636  bdth  14668  bdcdeq  14676  bdne  14690  bdreu  14692  bdcsn  14707  bdsep2  14723  bdsepnft  14724  bdsepnfALT  14726  bdbm1.3ii  14728  bj-nalset  14732  bj-zfpair2  14747  bj-bdfindes  14786  bj-nn0suc0  14787  bj-nntrans  14788  setindft  14802  setindis  14804  bdsetindis  14806  bj-inf2vnlem3  14809  bj-inf2vnlem4  14810  strcoll2  14820  strcollnft  14821  strcollnfALT  14823  sscoll2  14825  nnti  14829  nnsf  14839  peano4nninf  14840  nninfsellemqall  14849  nninfomni  14853  trilpolemeq1  14873  tridceq  14889  redc0  14890  reap0  14891  dceqnconst  14893  dcapnconst  14894  nconstwlpolemgt0  14897