Theorem weq 1552

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

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

Syntax hints:   = wceq 1398

This theorem is referenced by:  alequcoms  1565  equidqe  1581  ax4sp1  1582  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  1779  dral2  1780  drex2  1781  drnf1  1782  drnf2  1783  spimth  1784  spimh  1786  spimed  1789  cbv1  1794  cbv1h  1795  cbv1v  1796  cbv2h  1797  cbv2w  1799  cbvalv1  1800  cbvexv1  1801  cbvalh  1802  chvar  1806  sbimi  1813  sb1  1815  sb2  1816  sbequ1  1817  sbequ2  1818  sbequ12  1820  sbequ12r  1821  sbequ12a  1822  sbid  1823  stdpc4  1824  sbh  1825  sb6x  1828  sbequ5  1831  sbequ6  1832  equsb1  1834  equsb2  1835  sbiedh  1836  sbiedv  1838  sbieh  1839  equsalv  1842  equs5a  1843  drsb1  1848  exdistrfor  1849  sb4a  1850  equs45f  1851  sb6f  1852  sb5f  1853  sb4e  1854  hbsb2a  1855  hbsb2e  1856  sbcof2  1859  aev  1861  ax16  1862  dveeq2  1864  dveeq2or  1865  ax11v2  1869  ax11a2  1870  ax11b  1875  equs5  1878  equs5or  1879  sb3  1880  sb4  1881  sb4or  1882  sb4b  1883  sb4bor  1884  hbsb2  1885  nfsb2or  1886  sbequi  1888  sbequ  1889  drsb2  1890  spsbe  1891  spsbim  1892  sbequ8  1896  sbidm  1900  sb5rf  1901  sb6rf  1902  ax16i  1907  spv  1909  speiv  1911  equvin  1912  a16g  1913  a16gb  1914  a16nf  1915  equsv  1934  sb56  1936  sb6  1937  sb5  1938  sbnv  1939  sbanv  1940  sborv  1941  sbi1v  1942  sbi2v  1943  cbvalvw  1971  cbvexvw  1972  cbval2  1973  cbvex2  1974  cbvaldva  1980  cbvexdva  1981  cbvaldvaw  1982  cbval2vw  1984  cbvex2vw  1985  cbvex4v  1986  hbs1  1994  hbsbv  1997  nfsbxy  1998  nfsbxyt  1999  nfsbv  2003  equsb3  2007  sbco  2024  sbcocom  2026  sbcomxyyz  2028  sb9v  2034  2sb5  2039  2sb6  2040  sbcom2v  2041  sb6a  2044  2sb5rf  2045  2sb6rf  2046  dfsb7  2047  sb7f  2048  sb7af  2049  sb10f  2051  sbel2x  2054  sbalyz  2055  sbal1yz  2057  sbal1  2058  sbexyz  2059  exsb  2064  2exsb  2065  dvelimALT  2066  dvelimfv  2067  hbsb4t  2069  nfsb4t  2070  dvelimf  2071  dvelimdf  2072  dvelimor  2074  dveeq1  2075  sbal2  2076  euf  2087  eubidh  2088  eubid  2089  hbeu1  2092  nfeu1  2093  sb8eu  2095  nfeuv  2100  sb8euh  2105  eu1  2107  mo2n  2110  euex  2112  eumo0  2113  mo23  2124  mor  2125  modc  2126  eu2  2127  eu3h  2128  mo2r  2135  mo3h  2136  mo2dc  2138  mo4f  2143  eu4  2145  moim  2147  moimv  2149  moanim  2157  mopick  2161  2eu4  2176  euequ1  2178  exists1  2179  elequ1  2209  elequ2  2210  cleljust  2211  elsb1  2212  elsb2  2213  axext3  2217  axext4  2218  bm1.1  2219  eleq1w  2295  cleqh  2334  abbib  2352  cbvabw  2359  cbvab  2360  sbab  2364  nfcjust  2374  drnfc1  2403  drnfc2  2404  nfabdw  2405  dvelimdc  2407  dvelimc  2408  nfcvf  2409  cbvrmow  2729  cbvralfw  2769  cbvrexfw  2770  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvralvw  2784  cbvrexvw  2785  cbvreuvw  2786  cbvraldva2  2787  cbvrexdva2  2788  cbvraldva  2789  cbvrexdva  2790  cbvral2vw  2791  cbvrex2vw  2792  cbvral2v  2793  cbvrex2v  2794  cbvral3v  2795  sbralie  2798  cbvrab  2813  vjust  2816  vex  2818  rr19.3v  2958  rr19.28v  2959  ralab2  2983  rexab2  2985  reu2  3007  reu6  3008  reu3  3009  rmo4  3012  reu4  3013  reu7  3014  reu8  3015  rmo3f  3016  rmo4f  3017  cdeqi  3029  cdeqri  3030  cdeqth  3031  cdeqnot  3032  cdeqal  3033  cdeqab  3034  cdeqim  3037  cdeqcv  3038  cdeqeq  3039  cdeqel  3040  nfccdeq  3042  sbsbc  3048  sbc8g  3052  sbcco2  3067  sbc5  3068  sbcralt  3121  sbcralg  3123  sbcreug  3125  reu8nf  3126  rmo3  3137  cbvcsbw  3144  cbvcsb  3145  csbcow  3151  sbcel12g  3155  sbceqg  3156  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  difjust  3214  unjust  3216  injust  3218  dfss2f  3231  dfdif3  3331  dfnul3  3513  dfif3  3638  rabsnifsb  3759  preq12bg  3879  eluniab  3928  elintab  3962  int0  3965  dfiunv2  4029  cbviun  4030  cbviin  4031  cbvdisj  4097  invdisjrab  4105  disjiun  4106  sndisj  4107  sbcbrg  4166  cbvmptf  4206  cbvmpt  4207  axsep2  4231  bm1.3ii  4233  nalset  4242  zfpow  4290  el  4293  dtruarb  4306  copsexg  4362  opelopabsb  4380  swopo  4429  pofun  4435  issod  4442  frind  4475  zfun  4557  ruv  4674  dtru  4684  dcextest  4705  tfisi  4711  findes  4727  relop  4907  dfdmf  4951  dfrnf  5000  resiexg  5085  dfres2  5092  opabresid  5093  mptresid  5094  imai  5120  issref  5147  intasym  5149  cnvi  5169  rnxpid  5199  cnvpom  5307  nfiota1  5316  cbviota  5319  sb8iota  5322  iotaval  5326  iotanul  5330  iota4  5334  eliota  5342  eliotaeu  5343  csbiotag  5347  dffun2  5364  dffun4  5365  dffun5r  5366  dffun6f  5367  dffun4f  5370  sbcfung  5378  funopg  5388  fundif  5402  funinsn  5407  funcnveq  5421  fun11  5425  fununi  5426  funcnvuni  5427  imain  5440  isarep2  5445  brprcneu  5665  fv2  5667  elfv  5670  fv3  5695  relelfvdm  5704  fvmpt2  5763  ralrnmpt  5821  rexrnmpt  5822  ffnfvf  5838  f1veqaeq  5944  dff13f  5945  fliftfuns  5973  canth  6003  cbvriotavw  6016  cbvriota  6017  csbriotag  6019  acexmid  6051  oprabidlem  6083  cbvmpox  6133  cbvmpo  6134  cbvmpov  6135  mpofun  6157  abrexex2  6319  fmpoco  6414  f1o2ndf1  6426  poxp  6430  suppfnss  6459  tposoprab  6513  tfrlem3-2d  6545  tfrlemi1  6565  tfr1onlemsucfn  6573  tfr1onlemaccex  6581  tfrcllemsucfn  6586  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemaccex  6594  dcdifsnid  6739  fnsnsplitdc  6740  funresdfunsndc  6741  eqerlem  6800  qliftfuns  6855  eroveu  6862  cbvixp  6952  mptelixpg  6971  idssen  7018  modom  7063  pw2f1odclem  7089  xpf1o  7099  xpmapen  7105  findcard2d  7150  fidcen  7158  eqsndc  7165  nnwetri  7178  fiintim  7193  snexxph  7222  fidcenumlemim  7224  fidcenumlemrk  7226  fidcenum  7228  2omap  7271  supmoti  7286  isoti  7300  supisoti  7303  cnvti  7312  ordiso2  7328  ctssdccl  7404  finct  7409  infnninf  7417  nninfwlpoim  7472  nninfwlpo  7474  sspw1or2  7497  exmidontriimlem3  7532  exmidontriimlem4  7533  exmidontriim  7534  onntri13  7550  onntri51  7552  onntri3or  7557  dftap2  7567  netap  7570  2onetap  7571  2omotaplemap  7573  cc1  7581  cc2  7583  ltsopi  7637  addpipqqs  7687  mulpipqqs  7690  archpr  7960  cauappcvgprlemlol  7964  cauappcvgprlemopu  7965  cauappcvgprlemupu  7966  cauappcvgprlemdisj  7968  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlemlim  7978  caucvgprlemlol  7987  caucvgprlemopu  7988  caucvgprlemupu  7989  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemcl  7993  caucvgprlemladdrl  7995  caucvgprprlemcbv  8004  caucvgprprlemopu  8016  caucvgprprlemclphr  8022  caucvgprprlemexbt  8023  suplocexprlemmu  8035  suplocexprlemdisj  8037  caucvgsrlembound  8111  caucvgsrlembnd  8118  suplocsrlem  8125  suplocsr  8126  peano1nnnn  8169  axcaucvglemres  8216  axpre-suploc  8219  negf1o  8657  lbreu  9221  lbinf  9224  suprubex  9227  suprlubex  9228  suprleubex  9230  1nn  9250  zfidc  9658  uzind4s  9925  uzind4s2  9926  indstr  9928  supinfneg  9930  infsupneg  9931  infregelbex  9933  eqreznegel  9949  lbzbi  9951  elpq  9984  zsupcl  10595  infssuzex  10597  infssuzledc  10598  zsupssdc  10602  exbtwnzlemex  10613  exbtwnz  10614  rebtwn2zlemstep  10616  rebtwn2z  10618  iseqovex  10824  iseqvalcbv  10825  seqvalcd  10827  seqovcd  10833  seq3f1olemqsum  10879  seq3f1olemp  10881  seq3f1oleml  10882  seqf1og  10887  seq3distr  10898  faclbnd6  11110  fimaxq  11198  hashfibclem  11210  wrd2ind  11419  reuccatpfxs1lem  11442  reuccatpfxs1  11443  cvg1nlemres  11674  resqrexlemsqa  11713  resqrexlemex  11714  cau3lem  11803  fclim  11983  climeu  11985  cn1lem  12003  climcau  12036  climcvg1n  12039  summodclem3  12070  summodclem2a  12071  summodclem2  12072  summodc  12073  zsumdc  12074  fsum3  12077  isumz  12079  isumss2  12083  fsumsersdc  12085  fsum3ser  12087  fsumadd  12096  fsum2dlemstep  12124  fisumcom2  12128  isumshft  12180  cvgratz  12222  mertensabs  12227  prodfdivap  12237  cbvprod  12248  prodmodclem3  12265  prodmodclem2a  12266  prodmodclem2  12267  prodmodc  12268  zproddc  12269  fprodseq  12273  fprodm1s  12291  fprodp1s  12292  fprod2dlemstep  12312  fprodcom2fi  12316  fprodsplitf  12322  odd2np1lem  12562  bitsfzolem  12644  bezoutlemmain  12698  bezoutlemeu  12707  gcdmultiple  12720  rplpwr  12727  nnwofdc  12738  nnwosdc  12739  nninfctlemfo  12740  isprm5lem  12842  isprm5  12843  pw2dvdseu  12869  hashdvds  12922  eulerthlemh  12932  reumodprminv  12955  pclemub  12989  pclemdc  12990  pceu  12997  pcmptdvds  13047  1arith  13069  4sqlem2  13091  4sqlem11  13103  4sqlem12  13104  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemodife  13158  ennnfonelemg  13171  ennnfoneleminc  13179  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ennnfonelemex  13182  ennnfonelemhom  13183  ennnfonelemrnh  13184  ennnfonelemfun  13185  ennnfonelemdm  13188  ennnfonelemr  13191  ennnfone  13193  inffinp1  13197  ctinf  13198  nninfdclemf  13217  nninfdclemp1  13218  unbendc  13222  infpn2  13224  strsetsid  13262  mgmidmo  13602  lidrididd  13612  mndinvmod  13675  insubm  13715  dfgrp3mlem  13828  mulgaddcom  13880  mulginvcom  13881  isnsg2  13937  gsumfzconstf  14076  srgmulgass  14150  islmodd  14458  lmodvsmmulgdi  14488  rmodislmodlem  14515  rmodislmod  14516  lssats2  14579  mplsubgfilemcl  14871  baspartn  14932  cnpnei  15101  txdis1cn  15160  cnmptid  15163  xmetxp  15389  cncfmptc  15478  cncfmptid  15479  dedekindeulemloc  15501  dedekindicclemloc  15510  ivthinclemlr  15519  ivthinclemur  15521  ivthinclemloc  15523  ivthdec  15526  dvmptfsum  15607  plymullem1  15630  perfectlem2  15885  lgseisenlem2  15961  lgsquadlem3  15969  lgsquad  15970  lgsquad2lem2  15972  2lgslem1a  15978  usgruspgrben  16198  umgr2edg1  16221  umgr2edgneu  16224  usgredg4  16227  usgredgreu  16228  uspgredg2vtxeu  16230  vtxedgfi  16301  vtxlpfi  16302  depindlem1  16518  depindlem2  16519  depindlem3  16520  spimd  16554  2spim  16555  ch2var  16556  bj-sbimedh  16560  bj-sbimeh  16561  cbvrald  16577  sumdc2  16588  bdth  16618  bdcdeq  16626  bdne  16640  bdreu  16642  bdcsn  16657  bdsep2  16673  bdsepnft  16674  bdsepnfALT  16676  bdbm1.3ii  16678  bj-nalset  16682  bj-zfpair2  16697  bj-bdfindes  16736  bj-nn0suc0  16737  bj-nntrans  16738  setindft  16752  setindis  16754  bdsetindis  16756  bj-inf2vnlem3  16759  bj-inf2vnlem4  16760  strcoll2  16770  strcollnft  16771  strcollnfALT  16773  sscoll2  16775  nnti  16783  nnsf  16800  peano4nninf  16801  nninfsellemqall  16810  nninfomni  16814  nnnninfen  16816  repiecef  16829  trilpolemeq1  16841  tridceq  16858  redc0  16859  reap0  16860  dceqnconst  16863  dcapnconst  16864  nconstwlpolemgt0  16867