Theorem weq 1551

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

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

Syntax hints:   = wceq 1397

This theorem is referenced by:  alequcoms  1564  equidqe  1580  ax4sp1  1581  spimfv  1747  chvarfv  1748  equid  1749  nfequid  1750  stdpc6  1751  equcomi  1752  ax6evr  1753  equcom  1754  equcomd  1755  equcoms  1756  equtr  1757  equtrr  1758  equtr2  1759  equequ1  1760  equequ2  1761  ax11i  1762  ax10o  1763  ax10  1765  nfae  1767  hbaes  1768  hbnae  1769  nfnae  1770  hbnaes  1771  equsalh  1774  equsal  1775  dral1  1778  dral2  1779  drex2  1780  drnf1  1781  drnf2  1782  spimth  1783  spimh  1785  spimed  1788  cbv1  1793  cbv1h  1794  cbv1v  1795  cbv2h  1796  cbv2w  1798  cbvalv1  1799  cbvexv1  1800  cbvalh  1801  chvar  1805  sbimi  1812  sb1  1814  sb2  1815  sbequ1  1816  sbequ2  1817  sbequ12  1819  sbequ12r  1820  sbequ12a  1821  sbid  1822  stdpc4  1823  sbh  1824  sb6x  1827  sbequ5  1830  sbequ6  1831  equsb1  1833  equsb2  1834  sbiedh  1835  sbiedv  1837  sbieh  1838  equsalv  1841  equs5a  1842  drsb1  1847  exdistrfor  1848  sb4a  1849  equs45f  1850  sb6f  1851  sb5f  1852  sb4e  1853  hbsb2a  1854  hbsb2e  1855  sbcof2  1858  aev  1860  ax16  1861  dveeq2  1863  dveeq2or  1864  ax11v2  1868  ax11a2  1869  ax11b  1874  equs5  1877  equs5or  1878  sb3  1879  sb4  1880  sb4or  1881  sb4b  1882  sb4bor  1883  hbsb2  1884  nfsb2or  1885  sbequi  1887  sbequ  1888  drsb2  1889  spsbe  1890  spsbim  1891  sbequ8  1895  sbidm  1899  sb5rf  1900  sb6rf  1901  ax16i  1906  spv  1908  speiv  1910  equvin  1911  a16g  1912  a16gb  1913  a16nf  1914  sb56  1934  sb6  1935  sb5  1936  sbnv  1937  sbanv  1938  sborv  1939  sbi1v  1940  sbi2v  1941  cbvalvw  1968  cbvexvw  1969  cbval2  1970  cbvex2  1971  cbvaldva  1977  cbvexdva  1978  cbvaldvaw  1979  cbval2vw  1981  cbvex2vw  1982  cbvex4v  1983  hbs1  1991  hbsbv  1994  nfsbxy  1995  nfsbxyt  1996  nfsbv  2000  equsb3  2004  sbco  2021  sbcocom  2023  sbcomxyyz  2025  sb9v  2031  2sb5  2036  2sb6  2037  sbcom2v  2038  sb6a  2041  2sb5rf  2042  2sb6rf  2043  dfsb7  2044  sb7f  2045  sb7af  2046  sb10f  2048  sbel2x  2051  sbalyz  2052  sbal1yz  2054  sbal1  2055  sbexyz  2056  exsb  2061  2exsb  2062  dvelimALT  2063  dvelimfv  2064  hbsb4t  2066  nfsb4t  2067  dvelimf  2068  dvelimdf  2069  dvelimor  2071  dveeq1  2072  sbal2  2073  euf  2084  eubidh  2085  eubid  2086  hbeu1  2089  nfeu1  2090  sb8eu  2092  nfeuv  2097  sb8euh  2102  eu1  2104  mo2n  2107  euex  2109  eumo0  2110  mo23  2121  mor  2122  modc  2123  eu2  2124  eu3h  2125  mo2r  2132  mo3h  2133  mo2dc  2135  mo4f  2140  eu4  2142  moim  2144  moimv  2146  moanim  2154  mopick  2158  2eu4  2173  euequ1  2175  exists1  2176  elequ1  2206  elequ2  2207  cleljust  2208  elsb1  2209  elsb2  2210  axext3  2214  axext4  2215  bm1.1  2216  eleq1w  2292  cleqh  2331  cbvabw  2354  cbvab  2355  sbab  2359  nfcjust  2362  drnfc1  2391  drnfc2  2392  nfabdw  2393  dvelimdc  2395  dvelimc  2396  nfcvf  2397  cbvrmow  2716  cbvralfw  2756  cbvrexfw  2757  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvralvw  2771  cbvrexvw  2772  cbvreuvw  2773  cbvraldva2  2774  cbvrexdva2  2775  cbvraldva  2776  cbvrexdva  2777  cbvral2vw  2778  cbvrex2vw  2779  cbvral2v  2780  cbvrex2v  2781  cbvral3v  2782  sbralie  2785  cbvrab  2800  vjust  2803  vex  2805  rr19.3v  2945  rr19.28v  2946  ralab2  2970  rexab2  2972  reu2  2994  reu6  2995  reu3  2996  rmo4  2999  reu4  3000  reu7  3001  reu8  3002  rmo3f  3003  rmo4f  3004  cdeqi  3016  cdeqri  3017  cdeqth  3018  cdeqnot  3019  cdeqal  3020  cdeqab  3021  cdeqim  3024  cdeqcv  3025  cdeqeq  3026  cdeqel  3027  nfccdeq  3029  sbsbc  3035  sbc8g  3039  sbcco2  3054  sbc5  3055  sbcralt  3108  sbcralg  3110  sbcreug  3112  reu8nf  3113  rmo3  3124  cbvcsbw  3131  cbvcsb  3132  csbcow  3138  sbcel12g  3142  sbceqg  3143  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  difjust  3201  unjust  3203  injust  3205  dfss2f  3218  dfdif3  3317  dfnul3  3497  dfif3  3619  rabsnifsb  3737  preq12bg  3856  eluniab  3905  elintab  3939  int0  3942  dfiunv2  4006  cbviun  4007  cbviin  4008  cbvdisj  4074  invdisjrab  4082  disjiun  4083  sndisj  4084  sbcbrg  4143  cbvmptf  4183  cbvmpt  4184  axsep2  4208  bm1.3ii  4210  nalset  4219  zfpow  4265  el  4268  dtruarb  4281  copsexg  4336  opelopabsb  4354  swopo  4403  pofun  4409  issod  4416  frind  4449  zfun  4531  ruv  4648  dtru  4658  dcextest  4679  tfisi  4685  findes  4701  relop  4880  dfdmf  4924  dfrnf  4973  resiexg  5058  dfres2  5065  opabresid  5066  mptresid  5067  imai  5092  issref  5119  intasym  5121  cnvi  5141  rnxpid  5171  cnvpom  5279  nfiota1  5288  cbviota  5291  sb8iota  5294  iotaval  5298  iotanul  5302  iota4  5306  eliota  5314  eliotaeu  5315  csbiotag  5319  dffun2  5336  dffun4  5337  dffun5r  5338  dffun6f  5339  dffun4f  5342  sbcfung  5350  funopg  5360  fundif  5374  funinsn  5379  funcnveq  5393  fun11  5397  fununi  5398  funcnvuni  5399  imain  5412  isarep2  5417  brprcneu  5632  fv2  5634  elfv  5637  fv3  5662  relelfvdm  5671  fvmpt2  5730  ralrnmpt  5789  rexrnmpt  5790  ffnfvf  5806  f1veqaeq  5910  dff13f  5911  fliftfuns  5939  canth  5969  cbvriotavw  5982  cbvriota  5983  csbriotag  5985  acexmid  6017  oprabidlem  6049  cbvmpox  6099  cbvmpo  6100  cbvmpov  6101  mpofun  6123  abrexex2  6286  fmpoco  6381  f1o2ndf1  6393  poxp  6397  tposoprab  6446  tfrlem3-2d  6478  tfrlemi1  6498  tfr1onlemsucfn  6506  tfr1onlemaccex  6514  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  dcdifsnid  6672  fnsnsplitdc  6673  funresdfunsndc  6674  eqerlem  6733  qliftfuns  6788  eroveu  6795  cbvixp  6884  mptelixpg  6903  idssen  6950  modom  6994  pw2f1odclem  7020  xpf1o  7030  xpmapen  7036  findcard2d  7080  fidcen  7088  eqsndc  7095  nnwetri  7108  fiintim  7123  snexxph  7149  fidcenumlemim  7151  fidcenumlemrk  7153  fidcenum  7155  supmoti  7192  isoti  7206  supisoti  7209  cnvti  7218  ordiso2  7234  ctssdccl  7310  finct  7315  infnninf  7323  nninfwlpoim  7378  nninfwlpo  7380  sspw1or2  7403  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  onntri13  7456  onntri51  7458  onntri3or  7463  dftap2  7470  netap  7473  2onetap  7474  2omotaplemap  7476  cc1  7484  cc2  7486  ltsopi  7540  addpipqqs  7590  mulpipqqs  7593  archpr  7863  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlemlim  7881  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgprprlemcbv  7907  caucvgprprlemopu  7919  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  suplocexprlemmu  7938  suplocexprlemdisj  7940  caucvgsrlembound  8014  caucvgsrlembnd  8021  suplocsrlem  8028  suplocsr  8029  peano1nnnn  8072  axcaucvglemres  8119  axpre-suploc  8122  negf1o  8561  lbreu  9125  lbinf  9128  suprubex  9131  suprlubex  9132  suprleubex  9134  1nn  9154  uzind4s  9824  uzind4s2  9825  indstr  9827  supinfneg  9829  infsupneg  9830  infregelbex  9832  eqreznegel  9848  lbzbi  9850  elpq  9883  zsupcl  10492  infssuzex  10494  infssuzledc  10495  zsupssdc  10499  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  iseqovex  10721  iseqvalcbv  10722  seqvalcd  10724  seqovcd  10730  seq3f1olemqsum  10776  seq3f1olemp  10778  seq3f1oleml  10779  seqf1og  10784  seq3distr  10795  faclbnd6  11007  fimaxq  11092  wrd2ind  11308  reuccatpfxs1lem  11331  reuccatpfxs1  11332  cvg1nlemres  11563  resqrexlemsqa  11602  resqrexlemex  11603  cau3lem  11692  fclim  11872  climeu  11874  cn1lem  11892  climcau  11925  climcvg1n  11928  summodclem3  11959  summodclem2a  11960  summodclem2  11961  summodc  11962  zsumdc  11963  fsum3  11966  isumz  11968  isumss2  11972  fsumsersdc  11974  fsum3ser  11976  fsumadd  11985  fsum2dlemstep  12013  fisumcom2  12017  isumshft  12069  cvgratz  12111  mertensabs  12116  prodfdivap  12126  cbvprod  12137  prodmodclem3  12154  prodmodclem2a  12155  prodmodclem2  12156  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodm1s  12180  fprodp1s  12181  fprod2dlemstep  12201  fprodcom2fi  12205  fprodsplitf  12211  odd2np1lem  12451  bitsfzolem  12533  bezoutlemmain  12587  bezoutlemeu  12596  gcdmultiple  12609  rplpwr  12616  nnwofdc  12627  nnwosdc  12628  nninfctlemfo  12629  isprm5lem  12731  isprm5  12732  pw2dvdseu  12758  hashdvds  12811  eulerthlemh  12821  reumodprminv  12844  pclemub  12878  pclemdc  12879  pceu  12886  pcmptdvds  12936  1arith  12958  4sqlem2  12980  4sqlem11  12992  4sqlem12  12993  ennnfonelemg  13042  ennnfoneleminc  13050  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemrnh  13055  ennnfonelemfun  13056  ennnfonelemdm  13059  ennnfonelemr  13062  ennnfone  13064  inffinp1  13068  ctinf  13069  nninfdclemf  13088  nninfdclemp1  13089  unbendc  13093  infpn2  13095  strsetsid  13133  mgmidmo  13473  lidrididd  13483  mndinvmod  13546  insubm  13586  dfgrp3mlem  13699  mulgaddcom  13751  mulginvcom  13752  isnsg2  13808  gsumfzconstf  13947  srgmulgass  14021  islmodd  14326  lmodvsmmulgdi  14356  rmodislmodlem  14383  rmodislmod  14384  lssats2  14447  mplsubgfilemcl  14732  baspartn  14793  cnpnei  14962  txdis1cn  15021  cnmptid  15024  xmetxp  15250  cncfmptc  15339  cncfmptid  15340  dedekindeulemloc  15362  dedekindicclemloc  15371  ivthinclemlr  15380  ivthinclemur  15382  ivthinclemloc  15384  ivthdec  15387  dvmptfsum  15468  plymullem1  15491  perfectlem2  15743  lgseisenlem2  15819  lgsquadlem3  15827  lgsquad  15828  lgsquad2lem2  15830  2lgslem1a  15836  usgruspgrben  16056  umgr2edg1  16079  umgr2edgneu  16082  usgredg4  16085  usgredgreu  16086  uspgredg2vtxeu  16088  vtxedgfi  16159  vtxlpfi  16160  depindlem1  16376  depindlem2  16377  depindlem3  16378  spimd  16412  2spim  16413  ch2var  16414  bj-sbimedh  16418  bj-sbimeh  16419  cbvrald  16435  sumdc2  16446  bdth  16477  bdcdeq  16485  bdne  16499  bdreu  16501  bdcsn  16516  bdsep2  16532  bdsepnft  16533  bdsepnfALT  16535  bdbm1.3ii  16537  bj-nalset  16541  bj-zfpair2  16556  bj-bdfindes  16595  bj-nn0suc0  16596  bj-nntrans  16597  setindft  16611  setindis  16613  bdsetindis  16615  bj-inf2vnlem3  16618  bj-inf2vnlem4  16619  strcoll2  16629  strcollnft  16630  strcollnfALT  16632  sscoll2  16634  nnti  16642  2omap  16645  nnsf  16658  peano4nninf  16659  nninfsellemqall  16668  nninfomni  16672  nnnninfen  16674  trilpolemeq1  16695  tridceq  16712  redc0  16713  reap0  16714  dceqnconst  16716  dcapnconst  16717  nconstwlpolemgt0  16720