Theorem weq 1527

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

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

Syntax hints:   = wceq 1373

This theorem is referenced by:  alequcoms  1540  equidqe  1556  ax4sp1  1557  spimfv  1723  chvarfv  1724  equid  1725  nfequid  1726  stdpc6  1727  equcomi  1728  ax6evr  1729  equcom  1730  equcomd  1731  equcoms  1732  equtr  1733  equtrr  1734  equtr2  1735  equequ1  1736  equequ2  1737  ax11i  1738  ax10o  1739  ax10  1741  nfae  1743  hbaes  1744  hbnae  1745  nfnae  1746  hbnaes  1747  equsalh  1750  equsal  1751  dral1  1754  dral2  1755  drex2  1756  drnf1  1757  drnf2  1758  spimth  1759  spimh  1761  spimed  1764  cbv1  1769  cbv1h  1770  cbv1v  1771  cbv2h  1772  cbv2w  1774  cbvalv1  1775  cbvexv1  1776  cbvalh  1777  chvar  1781  sbimi  1788  sb1  1790  sb2  1791  sbequ1  1792  sbequ2  1793  sbequ12  1795  sbequ12r  1796  sbequ12a  1797  sbid  1798  stdpc4  1799  sbh  1800  sb6x  1803  sbequ5  1806  sbequ6  1807  equsb1  1809  equsb2  1810  sbiedh  1811  sbiedv  1813  sbieh  1814  equsalv  1817  equs5a  1818  drsb1  1823  exdistrfor  1824  sb4a  1825  equs45f  1826  sb6f  1827  sb5f  1828  sb4e  1829  hbsb2a  1830  hbsb2e  1831  sbcof2  1834  aev  1836  ax16  1837  dveeq2  1839  dveeq2or  1840  ax11v2  1844  ax11a2  1845  ax11b  1850  equs5  1853  equs5or  1854  sb3  1855  sb4  1856  sb4or  1857  sb4b  1858  sb4bor  1859  hbsb2  1860  nfsb2or  1861  sbequi  1863  sbequ  1864  drsb2  1865  spsbe  1866  spsbim  1867  sbequ8  1871  sbidm  1875  sb5rf  1876  sb6rf  1877  ax16i  1882  spv  1884  speiv  1886  equvin  1887  a16g  1888  a16gb  1889  a16nf  1890  sb56  1910  sb6  1911  sb5  1912  sbnv  1913  sbanv  1914  sborv  1915  sbi1v  1916  sbi2v  1917  cbvalvw  1944  cbvexvw  1945  cbval2  1946  cbvex2  1947  cbvaldva  1953  cbvexdva  1954  cbvaldvaw  1955  cbval2vw  1957  cbvex2vw  1958  cbvex4v  1959  hbs1  1967  hbsbv  1970  nfsbxy  1971  nfsbxyt  1972  nfsbv  1976  equsb3  1980  sbco  1997  sbcocom  1999  sbcomxyyz  2001  sb9v  2007  2sb5  2012  2sb6  2013  sbcom2v  2014  sb6a  2017  2sb5rf  2018  2sb6rf  2019  dfsb7  2020  sb7f  2021  sb7af  2022  sb10f  2024  sbel2x  2027  sbalyz  2028  sbal1yz  2030  sbal1  2031  sbexyz  2032  exsb  2037  2exsb  2038  dvelimALT  2039  dvelimfv  2040  hbsb4t  2042  nfsb4t  2043  dvelimf  2044  dvelimdf  2045  dvelimor  2047  dveeq1  2048  sbal2  2049  euf  2060  eubidh  2061  eubid  2062  hbeu1  2065  nfeu1  2066  sb8eu  2068  nfeuv  2073  sb8euh  2078  eu1  2080  mo2n  2083  euex  2085  eumo0  2086  mo23  2097  mor  2098  modc  2099  eu2  2100  eu3h  2101  mo2r  2108  mo3h  2109  mo2dc  2111  mo4f  2116  eu4  2118  moim  2120  moimv  2122  moanim  2130  mopick  2134  2eu4  2149  euequ1  2151  exists1  2152  elequ1  2182  elequ2  2183  cleljust  2184  elsb1  2185  elsb2  2186  axext3  2190  axext4  2191  bm1.1  2192  eleq1w  2268  cleqh  2307  cbvabw  2330  cbvab  2331  sbab  2335  nfcjust  2338  drnfc1  2367  drnfc2  2368  nfabdw  2369  dvelimdc  2371  dvelimc  2372  nfcvf  2373  cbvrmow  2691  cbvralfw  2731  cbvrexfw  2732  cbvralf  2733  cbvrexf  2734  cbvreu  2740  cbvralvw  2746  cbvrexvw  2747  cbvreuvw  2748  cbvraldva2  2749  cbvrexdva2  2750  cbvraldva  2751  cbvrexdva  2752  cbvral2vw  2753  cbvrex2vw  2754  cbvral2v  2755  cbvrex2v  2756  cbvral3v  2757  sbralie  2760  cbvrab  2774  vjust  2777  vex  2779  rr19.3v  2919  rr19.28v  2920  ralab2  2944  rexab2  2946  reu2  2968  reu6  2969  reu3  2970  rmo4  2973  reu4  2974  reu7  2975  reu8  2976  rmo3f  2977  rmo4f  2978  cdeqi  2990  cdeqri  2991  cdeqth  2992  cdeqnot  2993  cdeqal  2994  cdeqab  2995  cdeqim  2998  cdeqcv  2999  cdeqeq  3000  cdeqel  3001  nfccdeq  3003  sbsbc  3009  sbc8g  3013  sbcco2  3028  sbc5  3029  sbcralt  3082  sbcralg  3084  sbcreug  3086  reu8nf  3087  rmo3  3098  cbvcsbw  3105  cbvcsb  3106  csbcow  3112  sbcel12g  3116  sbceqg  3117  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  difjust  3175  unjust  3177  injust  3179  dfss2f  3192  dfdif3  3291  dfnul3  3471  dfif3  3593  preq12bg  3827  eluniab  3876  elintab  3910  int0  3913  dfiunv2  3977  cbviun  3978  cbviin  3979  cbvdisj  4045  invdisjrab  4053  disjiun  4054  sndisj  4055  sbcbrg  4114  cbvmptf  4154  cbvmpt  4155  axsep2  4179  bm1.3ii  4181  nalset  4190  zfpow  4235  el  4238  dtruarb  4251  copsexg  4306  opelopabsb  4324  swopo  4371  pofun  4377  issod  4384  frind  4417  zfun  4499  ruv  4616  dtru  4626  dcextest  4647  tfisi  4653  findes  4669  relop  4846  dfdmf  4890  dfrnf  4938  resiexg  5023  dfres2  5030  opabresid  5031  mptresid  5032  imai  5057  issref  5084  intasym  5086  cnvi  5106  rnxpid  5136  cnvpom  5244  nfiota1  5253  cbviota  5256  sb8iota  5258  iotaval  5262  iotanul  5266  iota4  5270  eliota  5278  eliotaeu  5279  csbiotag  5283  dffun2  5300  dffun4  5301  dffun5r  5302  dffun6f  5303  dffun4f  5306  sbcfung  5314  funopg  5324  fundif  5337  funinsn  5342  funcnveq  5356  fun11  5360  fununi  5361  funcnvuni  5362  imain  5375  isarep2  5380  brprcneu  5592  fv2  5594  elfv  5597  fv3  5622  relelfvdm  5631  fvmpt2  5686  ralrnmpt  5745  rexrnmpt  5746  ffnfvf  5762  f1veqaeq  5861  dff13f  5862  fliftfuns  5890  canth  5920  cbvriota  5933  csbriotag  5935  acexmid  5966  oprabidlem  5998  cbvmpox  6046  cbvmpo  6047  cbvmpov  6048  mpofun  6070  abrexex2  6232  fmpoco  6325  f1o2ndf1  6337  poxp  6341  tposoprab  6389  tfrlem3-2d  6421  tfrlemi1  6441  tfr1onlemsucfn  6449  tfr1onlemaccex  6457  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemaccex  6470  dcdifsnid  6613  fnsnsplitdc  6614  funresdfunsndc  6615  eqerlem  6674  qliftfuns  6729  eroveu  6736  cbvixp  6825  mptelixpg  6844  idssen  6891  pw2f1odclem  6956  xpf1o  6966  xpmapen  6972  findcard2d  7014  nnwetri  7039  fiintim  7054  snexxph  7078  fidcenumlemim  7080  fidcenumlemrk  7082  fidcenum  7084  supmoti  7121  isoti  7135  supisoti  7138  cnvti  7147  ordiso2  7163  ctssdccl  7239  finct  7244  infnninf  7252  nninfwlpoim  7307  nninfwlpo  7309  exmidontriimlem3  7366  exmidontriimlem4  7367  exmidontriim  7368  onntri13  7384  onntri51  7386  onntri3or  7391  dftap2  7398  netap  7401  2onetap  7402  2omotaplemap  7404  cc1  7412  cc2  7414  ltsopi  7468  addpipqqs  7518  mulpipqqs  7521  archpr  7791  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemdisj  7799  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlemlim  7809  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdrl  7826  caucvgprprlemcbv  7835  caucvgprprlemopu  7847  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  suplocexprlemmu  7866  suplocexprlemdisj  7868  caucvgsrlembound  7942  caucvgsrlembnd  7949  suplocsrlem  7956  suplocsr  7957  peano1nnnn  8000  axcaucvglemres  8047  axpre-suploc  8050  negf1o  8489  lbreu  9053  lbinf  9056  suprubex  9059  suprlubex  9060  suprleubex  9062  1nn  9082  uzind4s  9746  uzind4s2  9747  indstr  9749  supinfneg  9751  infsupneg  9752  infregelbex  9754  eqreznegel  9770  lbzbi  9772  elpq  9805  zsupcl  10411  infssuzex  10413  infssuzledc  10414  zsupssdc  10418  exbtwnzlemex  10429  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2z  10434  iseqovex  10640  iseqvalcbv  10641  seqvalcd  10643  seqovcd  10649  seq3f1olemqsum  10695  seq3f1olemp  10697  seq3f1oleml  10698  seqf1og  10703  seq3distr  10714  faclbnd6  10926  fimaxq  11009  wrd2ind  11214  reuccatpfxs1lem  11237  reuccatpfxs1  11238  cvg1nlemres  11411  resqrexlemsqa  11450  resqrexlemex  11451  cau3lem  11540  fclim  11720  climeu  11722  cn1lem  11740  climcau  11773  climcvg1n  11776  summodclem3  11806  summodclem2a  11807  summodclem2  11808  summodc  11809  zsumdc  11810  fsum3  11813  isumz  11815  isumss2  11819  fsumsersdc  11821  fsum3ser  11823  fsumadd  11832  fsum2dlemstep  11860  fisumcom2  11864  isumshft  11916  cvgratz  11958  mertensabs  11963  prodfdivap  11973  cbvprod  11984  prodmodclem3  12001  prodmodclem2a  12002  prodmodclem2  12003  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodm1s  12027  fprodp1s  12028  fprod2dlemstep  12048  fprodcom2fi  12052  fprodsplitf  12058  odd2np1lem  12298  bitsfzolem  12380  bezoutlemmain  12434  bezoutlemeu  12443  gcdmultiple  12456  rplpwr  12463  nnwofdc  12474  nnwosdc  12475  nninfctlemfo  12476  isprm5lem  12578  isprm5  12579  pw2dvdseu  12605  hashdvds  12658  eulerthlemh  12668  reumodprminv  12691  pclemub  12725  pclemdc  12726  pceu  12733  pcmptdvds  12783  1arith  12805  4sqlem2  12827  4sqlem11  12839  4sqlem12  12840  ennnfonelemg  12889  ennnfoneleminc  12897  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemrnh  12902  ennnfonelemfun  12903  ennnfonelemdm  12906  ennnfonelemr  12909  ennnfone  12911  inffinp1  12915  ctinf  12916  nninfdclemf  12935  nninfdclemp1  12936  unbendc  12940  infpn2  12942  strsetsid  12980  mgmidmo  13319  lidrididd  13329  mndinvmod  13392  insubm  13432  dfgrp3mlem  13545  mulgaddcom  13597  mulginvcom  13598  isnsg2  13654  gsumfzconstf  13793  srgmulgass  13866  islmodd  14170  lmodvsmmulgdi  14200  rmodislmodlem  14227  rmodislmod  14228  lssats2  14291  mplsubgfilemcl  14576  baspartn  14637  cnpnei  14806  txdis1cn  14865  cnmptid  14868  xmetxp  15094  cncfmptc  15183  cncfmptid  15184  dedekindeulemloc  15206  dedekindicclemloc  15215  ivthinclemlr  15224  ivthinclemur  15226  ivthinclemloc  15228  ivthdec  15231  dvmptfsum  15312  plymullem1  15335  perfectlem2  15587  lgseisenlem2  15663  lgsquadlem3  15671  lgsquad  15672  lgsquad2lem2  15674  2lgslem1a  15680  spimd  15901  2spim  15902  ch2var  15903  bj-sbimedh  15907  bj-sbimeh  15908  cbvrald  15924  sumdc2  15935  bdth  15966  bdcdeq  15974  bdne  15988  bdreu  15990  bdcsn  16005  bdsep2  16021  bdsepnft  16022  bdsepnfALT  16024  bdbm1.3ii  16026  bj-nalset  16030  bj-zfpair2  16045  bj-bdfindes  16084  bj-nn0suc0  16085  bj-nntrans  16086  setindft  16100  setindis  16102  bdsetindis  16104  bj-inf2vnlem3  16107  bj-inf2vnlem4  16108  strcoll2  16118  strcollnft  16119  strcollnfALT  16121  sscoll2  16123  nnti  16129  2omap  16132  nnsf  16144  peano4nninf  16145  nninfsellemqall  16154  nninfomni  16158  nnnninfen  16160  trilpolemeq1  16181  tridceq  16197  redc0  16198  reap0  16199  dceqnconst  16201  dcapnconst  16202  nconstwlpolemgt0  16205