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  invdisjrab  4039  disjiun  4040  sndisj  4041  sbcbrg  4099  cbvmptf  4139  cbvmpt  4140  axsep2  4164  bm1.3ii  4166  nalset  4175  zfpow  4220  el  4223  dtruarb  4236  copsexg  4289  opelopabsb  4307  swopo  4354  pofun  4360  issod  4367  frind  4400  zfun  4482  ruv  4599  dtru  4609  dcextest  4630  tfisi  4636  findes  4652  relop  4829  dfdmf  4872  dfrnf  4920  resiexg  5005  dfres2  5012  opabresid  5013  mptresid  5014  imai  5039  issref  5066  intasym  5068  cnvi  5088  rnxpid  5118  cnvpom  5226  nfiota1  5235  cbviota  5238  sb8iota  5240  iotaval  5244  iotanul  5248  iota4  5252  eliota  5260  eliotaeu  5261  csbiotag  5265  dffun2  5282  dffun4  5283  dffun5r  5284  dffun6f  5285  dffun4f  5288  sbcfung  5296  funopg  5306  fundif  5319  funinsn  5324  funcnveq  5338  fun11  5342  fununi  5343  funcnvuni  5344  imain  5357  isarep2  5362  brprcneu  5571  fv2  5573  elfv  5576  fv3  5601  relelfvdm  5610  fvmpt2  5665  ralrnmpt  5724  rexrnmpt  5725  ffnfvf  5741  f1veqaeq  5840  dff13f  5841  fliftfuns  5869  canth  5899  cbvriota  5912  csbriotag  5914  acexmid  5945  oprabidlem  5977  cbvmpox  6025  cbvmpo  6026  cbvmpov  6027  mpofun  6049  abrexex2  6211  fmpoco  6304  f1o2ndf1  6316  poxp  6320  tposoprab  6368  tfrlem3-2d  6400  tfrlemi1  6420  tfr1onlemsucfn  6428  tfr1onlemaccex  6436  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemaccex  6449  dcdifsnid  6592  fnsnsplitdc  6593  funresdfunsndc  6594  eqerlem  6653  qliftfuns  6708  eroveu  6715  cbvixp  6804  mptelixpg  6823  idssen  6870  pw2f1odclem  6933  xpf1o  6943  xpmapen  6949  findcard2d  6990  nnwetri  7015  fiintim  7030  snexxph  7054  fidcenumlemim  7056  fidcenumlemrk  7058  fidcenum  7060  supmoti  7097  isoti  7111  supisoti  7114  cnvti  7123  ordiso2  7139  ctssdccl  7215  finct  7220  infnninf  7228  nninfwlpoim  7283  nninfwlpo  7285  exmidontriimlem3  7337  exmidontriimlem4  7338  exmidontriim  7339  onntri13  7352  onntri51  7354  onntri3or  7359  dftap2  7365  netap  7368  2onetap  7369  2omotaplemap  7371  cc1  7379  cc2  7381  ltsopi  7435  addpipqqs  7485  mulpipqqs  7488  archpr  7758  cauappcvgprlemlol  7762  cauappcvgprlemopu  7763  cauappcvgprlemupu  7764  cauappcvgprlemdisj  7766  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlemlim  7776  caucvgprlemlol  7785  caucvgprlemopu  7786  caucvgprlemupu  7787  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdrl  7793  caucvgprprlemcbv  7802  caucvgprprlemopu  7814  caucvgprprlemclphr  7820  caucvgprprlemexbt  7821  suplocexprlemmu  7833  suplocexprlemdisj  7835  caucvgsrlembound  7909  caucvgsrlembnd  7916  suplocsrlem  7923  suplocsr  7924  peano1nnnn  7967  axcaucvglemres  8014  axpre-suploc  8017  negf1o  8456  lbreu  9020  lbinf  9023  suprubex  9026  suprlubex  9027  suprleubex  9029  1nn  9049  uzind4s  9713  uzind4s2  9714  indstr  9716  supinfneg  9718  infsupneg  9719  infregelbex  9721  eqreznegel  9737  lbzbi  9739  elpq  9772  zsupcl  10376  infssuzex  10378  infssuzledc  10379  zsupssdc  10383  exbtwnzlemex  10394  exbtwnz  10395  rebtwn2zlemstep  10397  rebtwn2z  10399  iseqovex  10605  iseqvalcbv  10606  seqvalcd  10608  seqovcd  10614  seq3f1olemqsum  10660  seq3f1olemp  10662  seq3f1oleml  10663  seqf1og  10668  seq3distr  10679  faclbnd6  10891  fimaxq  10974  cvg1nlemres  11329  resqrexlemsqa  11368  resqrexlemex  11369  cau3lem  11458  fclim  11638  climeu  11640  cn1lem  11658  climcau  11691  climcvg1n  11694  summodclem3  11724  summodclem2a  11725  summodclem2  11726  summodc  11727  zsumdc  11728  fsum3  11731  isumz  11733  isumss2  11737  fsumsersdc  11739  fsum3ser  11741  fsumadd  11750  fsum2dlemstep  11778  fisumcom2  11782  isumshft  11834  cvgratz  11876  mertensabs  11881  prodfdivap  11891  cbvprod  11902  prodmodclem3  11919  prodmodclem2a  11920  prodmodclem2  11921  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodm1s  11945  fprodp1s  11946  fprod2dlemstep  11966  fprodcom2fi  11970  fprodsplitf  11976  odd2np1lem  12216  bitsfzolem  12298  bezoutlemmain  12352  bezoutlemeu  12361  gcdmultiple  12374  rplpwr  12381  nnwofdc  12392  nnwosdc  12393  nninfctlemfo  12394  isprm5lem  12496  isprm5  12497  pw2dvdseu  12523  hashdvds  12576  eulerthlemh  12586  reumodprminv  12609  pclemub  12643  pclemdc  12644  pceu  12651  pcmptdvds  12701  1arith  12723  4sqlem2  12745  4sqlem11  12757  4sqlem12  12758  ennnfonelemg  12807  ennnfoneleminc  12815  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemrnh  12820  ennnfonelemfun  12821  ennnfonelemdm  12824  ennnfonelemr  12827  ennnfone  12829  inffinp1  12833  ctinf  12834  nninfdclemf  12853  nninfdclemp1  12854  unbendc  12858  infpn2  12860  strsetsid  12898  mgmidmo  13237  lidrididd  13247  mndinvmod  13310  insubm  13350  dfgrp3mlem  13463  mulgaddcom  13515  mulginvcom  13516  isnsg2  13572  gsumfzconstf  13711  srgmulgass  13784  islmodd  14088  lmodvsmmulgdi  14118  rmodislmodlem  14145  rmodislmod  14146  lssats2  14209  mplsubgfilemcl  14494  baspartn  14555  cnpnei  14724  txdis1cn  14783  cnmptid  14786  xmetxp  15012  cncfmptc  15101  cncfmptid  15102  dedekindeulemloc  15124  dedekindicclemloc  15133  ivthinclemlr  15142  ivthinclemur  15144  ivthinclemloc  15146  ivthdec  15149  dvmptfsum  15230  plymullem1  15253  perfectlem2  15505  lgseisenlem2  15581  lgsquadlem3  15589  lgsquad  15590  lgsquad2lem2  15592  2lgslem1a  15598  spimd  15738  2spim  15739  ch2var  15740  bj-sbimedh  15744  bj-sbimeh  15745  cbvrald  15761  sumdc2  15772  bdth  15804  bdcdeq  15812  bdne  15826  bdreu  15828  bdcsn  15843  bdsep2  15859  bdsepnft  15860  bdsepnfALT  15862  bdbm1.3ii  15864  bj-nalset  15868  bj-zfpair2  15883  bj-bdfindes  15922  bj-nn0suc0  15923  bj-nntrans  15924  setindft  15938  setindis  15940  bdsetindis  15942  bj-inf2vnlem3  15945  bj-inf2vnlem4  15946  strcoll2  15956  strcollnft  15957  strcollnfALT  15959  sscoll2  15961  nnti  15966  2omap  15969  nnsf  15979  peano4nninf  15980  nninfsellemqall  15989  nninfomni  15993  nnnninfen  15995  trilpolemeq1  16016  tridceq  16032  redc0  16033  reap0  16034  dceqnconst  16036  dcapnconst  16037  nconstwlpolemgt0  16040