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  5909  dff13f  5910  fliftfuns  5938  canth  5968  cbvriotavw  5981  cbvriota  5982  csbriotag  5984  acexmid  6016  oprabidlem  6048  cbvmpox  6098  cbvmpo  6099  cbvmpov  6100  mpofun  6122  abrexex2  6285  fmpoco  6380  f1o2ndf1  6392  poxp  6396  tposoprab  6445  tfrlem3-2d  6477  tfrlemi1  6497  tfr1onlemsucfn  6505  tfr1onlemaccex  6513  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  dcdifsnid  6671  fnsnsplitdc  6672  funresdfunsndc  6673  eqerlem  6732  qliftfuns  6787  eroveu  6794  cbvixp  6883  mptelixpg  6902  idssen  6949  modom  6993  pw2f1odclem  7019  xpf1o  7029  xpmapen  7035  findcard2d  7079  fidcen  7087  eqsndc  7094  nnwetri  7107  fiintim  7122  snexxph  7148  fidcenumlemim  7150  fidcenumlemrk  7152  fidcenum  7154  supmoti  7191  isoti  7205  supisoti  7208  cnvti  7217  ordiso2  7233  ctssdccl  7309  finct  7314  infnninf  7322  nninfwlpoim  7377  nninfwlpo  7379  sspw1or2  7402  exmidontriimlem3  7437  exmidontriimlem4  7438  exmidontriim  7439  onntri13  7455  onntri51  7457  onntri3or  7462  dftap2  7469  netap  7472  2onetap  7473  2omotaplemap  7475  cc1  7483  cc2  7485  ltsopi  7539  addpipqqs  7589  mulpipqqs  7592  archpr  7862  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlemlim  7880  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdrl  7897  caucvgprprlemcbv  7906  caucvgprprlemopu  7918  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  suplocexprlemmu  7937  suplocexprlemdisj  7939  caucvgsrlembound  8013  caucvgsrlembnd  8020  suplocsrlem  8027  suplocsr  8028  peano1nnnn  8071  axcaucvglemres  8118  axpre-suploc  8121  negf1o  8560  lbreu  9124  lbinf  9127  suprubex  9130  suprlubex  9131  suprleubex  9133  1nn  9153  uzind4s  9823  uzind4s2  9824  indstr  9826  supinfneg  9828  infsupneg  9829  infregelbex  9831  eqreznegel  9847  lbzbi  9849  elpq  9882  zsupcl  10490  infssuzex  10492  infssuzledc  10493  zsupssdc  10497  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2z  10513  iseqovex  10719  iseqvalcbv  10720  seqvalcd  10722  seqovcd  10728  seq3f1olemqsum  10774  seq3f1olemp  10776  seq3f1oleml  10777  seqf1og  10782  seq3distr  10793  faclbnd6  11005  fimaxq  11090  wrd2ind  11303  reuccatpfxs1lem  11326  reuccatpfxs1  11327  cvg1nlemres  11545  resqrexlemsqa  11584  resqrexlemex  11585  cau3lem  11674  fclim  11854  climeu  11856  cn1lem  11874  climcau  11907  climcvg1n  11910  summodclem3  11940  summodclem2a  11941  summodclem2  11942  summodc  11943  zsumdc  11944  fsum3  11947  isumz  11949  isumss2  11953  fsumsersdc  11955  fsum3ser  11957  fsumadd  11966  fsum2dlemstep  11994  fisumcom2  11998  isumshft  12050  cvgratz  12092  mertensabs  12097  prodfdivap  12107  cbvprod  12118  prodmodclem3  12135  prodmodclem2a  12136  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodm1s  12161  fprodp1s  12162  fprod2dlemstep  12182  fprodcom2fi  12186  fprodsplitf  12192  odd2np1lem  12432  bitsfzolem  12514  bezoutlemmain  12568  bezoutlemeu  12577  gcdmultiple  12590  rplpwr  12597  nnwofdc  12608  nnwosdc  12609  nninfctlemfo  12610  isprm5lem  12712  isprm5  12713  pw2dvdseu  12739  hashdvds  12792  eulerthlemh  12802  reumodprminv  12825  pclemub  12859  pclemdc  12860  pceu  12867  pcmptdvds  12917  1arith  12939  4sqlem2  12961  4sqlem11  12973  4sqlem12  12974  ennnfonelemg  13023  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemrnh  13036  ennnfonelemfun  13037  ennnfonelemdm  13040  ennnfonelemr  13043  ennnfone  13045  inffinp1  13049  ctinf  13050  nninfdclemf  13069  nninfdclemp1  13070  unbendc  13074  infpn2  13076  strsetsid  13114  mgmidmo  13454  lidrididd  13464  mndinvmod  13527  insubm  13567  dfgrp3mlem  13680  mulgaddcom  13732  mulginvcom  13733  isnsg2  13789  gsumfzconstf  13928  srgmulgass  14001  islmodd  14306  lmodvsmmulgdi  14336  rmodislmodlem  14363  rmodislmod  14364  lssats2  14427  mplsubgfilemcl  14712  baspartn  14773  cnpnei  14942  txdis1cn  15001  cnmptid  15004  xmetxp  15230  cncfmptc  15319  cncfmptid  15320  dedekindeulemloc  15342  dedekindicclemloc  15351  ivthinclemlr  15360  ivthinclemur  15362  ivthinclemloc  15364  ivthdec  15367  dvmptfsum  15448  plymullem1  15471  perfectlem2  15723  lgseisenlem2  15799  lgsquadlem3  15807  lgsquad  15808  lgsquad2lem2  15810  2lgslem1a  15816  usgruspgrben  16036  umgr2edg1  16059  umgr2edgneu  16062  usgredg4  16065  usgredgreu  16066  uspgredg2vtxeu  16068  vtxedgfi  16139  vtxlpfi  16140  spimd  16361  2spim  16362  ch2var  16363  bj-sbimedh  16367  bj-sbimeh  16368  cbvrald  16384  sumdc2  16395  bdth  16426  bdcdeq  16434  bdne  16448  bdreu  16450  bdcsn  16465  bdsep2  16481  bdsepnft  16482  bdsepnfALT  16484  bdbm1.3ii  16486  bj-nalset  16490  bj-zfpair2  16505  bj-bdfindes  16544  bj-nn0suc0  16545  bj-nntrans  16546  setindft  16560  setindis  16562  bdsetindis  16564  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568  strcoll2  16578  strcollnft  16579  strcollnfALT  16581  sscoll2  16583  nnti  16591  2omap  16594  nnsf  16607  peano4nninf  16608  nninfsellemqall  16617  nninfomni  16621  nnnninfen  16623  trilpolemeq1  16644  tridceq  16660  redc0  16661  reap0  16662  dceqnconst  16664  dcapnconst  16665  nconstwlpolemgt0  16668