Theorem weq 1526

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

(Instead of introducing weq 1526 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 1526 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  1539  equidqe  1555  ax4sp1  1556  spimfv  1722  chvarfv  1723  equid  1724  nfequid  1725  stdpc6  1726  equcomi  1727  ax6evr  1728  equcom  1729  equcomd  1730  equcoms  1731  equtr  1732  equtrr  1733  equtr2  1734  equequ1  1735  equequ2  1736  ax11i  1737  ax10o  1738  ax10  1740  nfae  1742  hbaes  1743  hbnae  1744  nfnae  1745  hbnaes  1746  equsalh  1749  equsal  1750  dral1  1753  dral2  1754  drex2  1755  drnf1  1756  drnf2  1757  spimth  1758  spimh  1760  spimed  1763  cbv1  1768  cbv1h  1769  cbv1v  1770  cbv2h  1771  cbv2w  1773  cbvalv1  1774  cbvexv1  1775  cbvalh  1776  chvar  1780  sbimi  1787  sb1  1789  sb2  1790  sbequ1  1791  sbequ2  1792  sbequ12  1794  sbequ12r  1795  sbequ12a  1796  sbid  1797  stdpc4  1798  sbh  1799  sb6x  1802  sbequ5  1805  sbequ6  1806  equsb1  1808  equsb2  1809  sbiedh  1810  sbiedv  1812  sbieh  1813  equsalv  1816  equs5a  1817  drsb1  1822  exdistrfor  1823  sb4a  1824  equs45f  1825  sb6f  1826  sb5f  1827  sb4e  1828  hbsb2a  1829  hbsb2e  1830  sbcof2  1833  aev  1835  ax16  1836  dveeq2  1838  dveeq2or  1839  ax11v2  1843  ax11a2  1844  ax11b  1849  equs5  1852  equs5or  1853  sb3  1854  sb4  1855  sb4or  1856  sb4b  1857  sb4bor  1858  hbsb2  1859  nfsb2or  1860  sbequi  1862  sbequ  1863  drsb2  1864  spsbe  1865  spsbim  1866  sbequ8  1870  sbidm  1874  sb5rf  1875  sb6rf  1876  ax16i  1881  spv  1883  speiv  1885  equvin  1886  a16g  1887  a16gb  1888  a16nf  1889  sb56  1909  sb6  1910  sb5  1911  sbnv  1912  sbanv  1913  sborv  1914  sbi1v  1915  sbi2v  1916  cbvalvw  1943  cbvexvw  1944  cbval2  1945  cbvex2  1946  cbvaldva  1952  cbvexdva  1953  cbvaldvaw  1954  cbval2vw  1956  cbvex2vw  1957  cbvex4v  1958  hbs1  1966  hbsbv  1969  nfsbxy  1970  nfsbxyt  1971  nfsbv  1975  equsb3  1979  sbco  1996  sbcocom  1998  sbcomxyyz  2000  sb9v  2006  2sb5  2011  2sb6  2012  sbcom2v  2013  sb6a  2016  2sb5rf  2017  2sb6rf  2018  dfsb7  2019  sb7f  2020  sb7af  2021  sb10f  2023  sbel2x  2026  sbalyz  2027  sbal1yz  2029  sbal1  2030  sbexyz  2031  exsb  2036  2exsb  2037  dvelimALT  2038  dvelimfv  2039  hbsb4t  2041  nfsb4t  2042  dvelimf  2043  dvelimdf  2044  dvelimor  2046  dveeq1  2047  sbal2  2048  euf  2059  eubidh  2060  eubid  2061  hbeu1  2064  nfeu1  2065  sb8eu  2067  nfeuv  2072  sb8euh  2077  eu1  2079  mo2n  2082  euex  2084  eumo0  2085  mo23  2095  mor  2096  modc  2097  eu2  2098  eu3h  2099  mo2r  2106  mo3h  2107  mo2dc  2109  mo4f  2114  eu4  2116  moim  2118  moimv  2120  moanim  2128  mopick  2132  2eu4  2147  euequ1  2149  exists1  2150  elequ1  2180  elequ2  2181  cleljust  2182  elsb1  2183  elsb2  2184  axext3  2188  axext4  2189  bm1.1  2190  eleq1w  2266  cleqh  2305  cbvabw  2328  cbvab  2329  sbab  2333  nfcjust  2336  drnfc1  2365  drnfc2  2366  nfabdw  2367  dvelimdc  2369  dvelimc  2370  nfcvf  2371  cbvralfw  2728  cbvrexfw  2729  cbvralf  2730  cbvrexf  2731  cbvreu  2736  cbvralvw  2742  cbvrexvw  2743  cbvreuvw  2744  cbvraldva2  2745  cbvrexdva2  2746  cbvraldva  2747  cbvrexdva  2748  cbvral2vw  2749  cbvrex2vw  2750  cbvral2v  2751  cbvrex2v  2752  cbvral3v  2753  sbralie  2756  cbvrab  2770  vjust  2773  vex  2775  rr19.3v  2912  rr19.28v  2913  ralab2  2937  rexab2  2939  reu2  2961  reu6  2962  reu3  2963  rmo4  2966  reu4  2967  reu7  2968  reu8  2969  rmo3f  2970  rmo4f  2971  cdeqi  2983  cdeqri  2984  cdeqth  2985  cdeqnot  2986  cdeqal  2987  cdeqab  2988  cdeqim  2991  cdeqcv  2992  cdeqeq  2993  cdeqel  2994  nfccdeq  2996  sbsbc  3002  sbc8g  3006  sbcco2  3021  sbc5  3022  sbcralt  3075  sbcralg  3077  sbcreug  3079  rmo3  3090  cbvcsbw  3097  cbvcsb  3098  csbcow  3104  sbcel12g  3108  sbceqg  3109  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  difjust  3167  unjust  3169  injust  3171  dfss2f  3184  dfdif3  3283  dfnul3  3463  dfif3  3584  preq12bg  3814  eluniab  3862  elintab  3896  int0  3899  dfiunv2  3963  cbviun  3964  cbviin  3965  cbvdisj  4031  disjiun  4039  sndisj  4040  sbcbrg  4098  cbvmptf  4138  cbvmpt  4139  axsep2  4163  bm1.3ii  4165  nalset  4174  zfpow  4219  el  4222  dtruarb  4235  copsexg  4288  opelopabsb  4306  swopo  4353  pofun  4359  issod  4366  frind  4399  zfun  4481  ruv  4598  dtru  4608  dcextest  4629  tfisi  4635  findes  4651  relop  4828  dfdmf  4871  dfrnf  4919  resiexg  5004  dfres2  5011  opabresid  5012  mptresid  5013  imai  5038  issref  5065  intasym  5067  cnvi  5087  rnxpid  5117  cnvpom  5225  nfiota1  5234  cbviota  5237  sb8iota  5239  iotaval  5243  iotanul  5247  iota4  5251  eliota  5259  eliotaeu  5260  csbiotag  5264  dffun2  5281  dffun4  5282  dffun5r  5283  dffun6f  5284  dffun4f  5287  sbcfung  5295  funopg  5305  fundif  5318  funinsn  5323  funcnveq  5337  fun11  5341  fununi  5342  funcnvuni  5343  imain  5356  isarep2  5361  brprcneu  5569  fv2  5571  elfv  5574  fv3  5599  relelfvdm  5608  fvmpt2  5663  ralrnmpt  5722  rexrnmpt  5723  ffnfvf  5739  f1veqaeq  5838  dff13f  5839  fliftfuns  5867  canth  5897  cbvriota  5910  csbriotag  5912  acexmid  5943  oprabidlem  5975  cbvmpox  6023  cbvmpo  6024  cbvmpov  6025  mpofun  6047  abrexex2  6209  fmpoco  6302  f1o2ndf1  6314  poxp  6318  tposoprab  6366  tfrlem3-2d  6398  tfrlemi1  6418  tfr1onlemsucfn  6426  tfr1onlemaccex  6434  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemaccex  6447  dcdifsnid  6590  fnsnsplitdc  6591  funresdfunsndc  6592  eqerlem  6651  qliftfuns  6706  eroveu  6713  cbvixp  6802  mptelixpg  6821  idssen  6868  pw2f1odclem  6931  xpf1o  6941  xpmapen  6947  findcard2d  6988  nnwetri  7013  fiintim  7028  snexxph  7052  fidcenumlemim  7054  fidcenumlemrk  7056  fidcenum  7058  supmoti  7095  isoti  7109  supisoti  7112  cnvti  7121  ordiso2  7137  ctssdccl  7213  finct  7218  infnninf  7226  nninfwlpoim  7281  nninfwlpo  7283  exmidontriimlem3  7335  exmidontriimlem4  7336  exmidontriim  7337  onntri13  7350  onntri51  7352  onntri3or  7357  dftap2  7363  netap  7366  2onetap  7367  2omotaplemap  7369  cc1  7377  cc2  7379  ltsopi  7433  addpipqqs  7483  mulpipqqs  7486  archpr  7756  cauappcvgprlemlol  7760  cauappcvgprlemopu  7761  cauappcvgprlemupu  7762  cauappcvgprlemdisj  7764  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlemlim  7774  caucvgprlemlol  7783  caucvgprlemopu  7784  caucvgprlemupu  7785  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdrl  7791  caucvgprprlemcbv  7800  caucvgprprlemopu  7812  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  suplocexprlemmu  7831  suplocexprlemdisj  7833  caucvgsrlembound  7907  caucvgsrlembnd  7914  suplocsrlem  7921  suplocsr  7922  peano1nnnn  7965  axcaucvglemres  8012  axpre-suploc  8015  negf1o  8454  lbreu  9018  lbinf  9021  suprubex  9024  suprlubex  9025  suprleubex  9027  1nn  9047  uzind4s  9711  uzind4s2  9712  indstr  9714  supinfneg  9716  infsupneg  9717  infregelbex  9719  eqreznegel  9735  lbzbi  9737  elpq  9770  zsupcl  10374  infssuzex  10376  infssuzledc  10377  zsupssdc  10381  exbtwnzlemex  10392  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2z  10397  iseqovex  10603  iseqvalcbv  10604  seqvalcd  10606  seqovcd  10612  seq3f1olemqsum  10658  seq3f1olemp  10660  seq3f1oleml  10661  seqf1og  10666  seq3distr  10677  faclbnd6  10889  fimaxq  10972  cvg1nlemres  11296  resqrexlemsqa  11335  resqrexlemex  11336  cau3lem  11425  fclim  11605  climeu  11607  cn1lem  11625  climcau  11658  climcvg1n  11661  summodclem3  11691  summodclem2a  11692  summodclem2  11693  summodc  11694  zsumdc  11695  fsum3  11698  isumz  11700  isumss2  11704  fsumsersdc  11706  fsum3ser  11708  fsumadd  11717  fsum2dlemstep  11745  fisumcom2  11749  isumshft  11801  cvgratz  11843  mertensabs  11848  prodfdivap  11858  cbvprod  11869  prodmodclem3  11886  prodmodclem2a  11887  prodmodclem2  11888  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodm1s  11912  fprodp1s  11913  fprod2dlemstep  11933  fprodcom2fi  11937  fprodsplitf  11943  odd2np1lem  12183  bitsfzolem  12265  bezoutlemmain  12319  bezoutlemeu  12328  gcdmultiple  12341  rplpwr  12348  nnwofdc  12359  nnwosdc  12360  nninfctlemfo  12361  isprm5lem  12463  isprm5  12464  pw2dvdseu  12490  hashdvds  12543  eulerthlemh  12553  reumodprminv  12576  pclemub  12610  pclemdc  12611  pceu  12618  pcmptdvds  12668  1arith  12690  4sqlem2  12712  4sqlem11  12724  4sqlem12  12725  ennnfonelemg  12774  ennnfoneleminc  12782  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemrnh  12787  ennnfonelemfun  12788  ennnfonelemdm  12791  ennnfonelemr  12794  ennnfone  12796  inffinp1  12800  ctinf  12801  nninfdclemf  12820  nninfdclemp1  12821  unbendc  12825  infpn2  12827  strsetsid  12865  mgmidmo  13204  lidrididd  13214  mndinvmod  13277  insubm  13317  dfgrp3mlem  13430  mulgaddcom  13482  mulginvcom  13483  isnsg2  13539  gsumfzconstf  13678  srgmulgass  13751  islmodd  14055  lmodvsmmulgdi  14085  rmodislmodlem  14112  rmodislmod  14113  lssats2  14176  mplsubgfilemcl  14461  baspartn  14522  cnpnei  14691  txdis1cn  14750  cnmptid  14753  xmetxp  14979  cncfmptc  15068  cncfmptid  15069  dedekindeulemloc  15091  dedekindicclemloc  15100  ivthinclemlr  15109  ivthinclemur  15111  ivthinclemloc  15113  ivthdec  15116  dvmptfsum  15197  plymullem1  15220  perfectlem2  15472  lgseisenlem2  15548  lgsquadlem3  15556  lgsquad  15557  lgsquad2lem2  15559  2lgslem1a  15565  spimd  15701  2spim  15702  ch2var  15703  bj-sbimedh  15707  bj-sbimeh  15708  cbvrald  15724  sumdc2  15735  bdth  15767  bdcdeq  15775  bdne  15789  bdreu  15791  bdcsn  15806  bdsep2  15822  bdsepnft  15823  bdsepnfALT  15825  bdbm1.3ii  15827  bj-nalset  15831  bj-zfpair2  15846  bj-bdfindes  15885  bj-nn0suc0  15886  bj-nntrans  15887  setindft  15901  setindis  15903  bdsetindis  15905  bj-inf2vnlem3  15908  bj-inf2vnlem4  15909  strcoll2  15919  strcollnft  15920  strcollnfALT  15922  sscoll2  15924  nnti  15929  2omap  15932  nnsf  15942  peano4nninf  15943  nninfsellemqall  15952  nninfomni  15956  nnnninfen  15958  trilpolemeq1  15979  tridceq  15995  redc0  15996  reap0  15997  dceqnconst  15999  dcapnconst  16000  nconstwlpolemgt0  16003