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  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  abbib  2349  cbvabw  2355  cbvab  2356  sbab  2360  nfcjust  2363  drnfc1  2392  drnfc2  2393  nfabdw  2394  dvelimdc  2396  dvelimc  2397  nfcvf  2398  cbvrmow  2717  cbvralfw  2757  cbvrexfw  2758  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvralvw  2772  cbvrexvw  2773  cbvreuvw  2774  cbvraldva2  2775  cbvrexdva2  2776  cbvraldva  2777  cbvrexdva  2778  cbvral2vw  2779  cbvrex2vw  2780  cbvral2v  2781  cbvrex2v  2782  cbvral3v  2783  sbralie  2786  cbvrab  2801  vjust  2804  vex  2806  rr19.3v  2946  rr19.28v  2947  ralab2  2971  rexab2  2973  reu2  2995  reu6  2996  reu3  2997  rmo4  3000  reu4  3001  reu7  3002  reu8  3003  rmo3f  3004  rmo4f  3005  cdeqi  3017  cdeqri  3018  cdeqth  3019  cdeqnot  3020  cdeqal  3021  cdeqab  3022  cdeqim  3025  cdeqcv  3026  cdeqeq  3027  cdeqel  3028  nfccdeq  3030  sbsbc  3036  sbc8g  3040  sbcco2  3055  sbc5  3056  sbcralt  3109  sbcralg  3111  sbcreug  3113  reu8nf  3114  rmo3  3125  cbvcsbw  3132  cbvcsb  3133  csbcow  3139  sbcel12g  3143  sbceqg  3144  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  difjust  3202  unjust  3204  injust  3206  dfss2f  3219  dfdif3  3319  dfnul3  3499  dfif3  3623  rabsnifsb  3741  preq12bg  3861  eluniab  3910  elintab  3944  int0  3947  dfiunv2  4011  cbviun  4012  cbviin  4013  cbvdisj  4079  invdisjrab  4087  disjiun  4088  sndisj  4089  sbcbrg  4148  cbvmptf  4188  cbvmpt  4189  axsep2  4213  bm1.3ii  4215  nalset  4224  zfpow  4271  el  4274  dtruarb  4287  copsexg  4342  opelopabsb  4360  swopo  4409  pofun  4415  issod  4422  frind  4455  zfun  4537  ruv  4654  dtru  4664  dcextest  4685  tfisi  4691  findes  4707  relop  4886  dfdmf  4930  dfrnf  4979  resiexg  5064  dfres2  5071  opabresid  5072  mptresid  5073  imai  5099  issref  5126  intasym  5128  cnvi  5148  rnxpid  5178  cnvpom  5286  nfiota1  5295  cbviota  5298  sb8iota  5301  iotaval  5305  iotanul  5309  iota4  5313  eliota  5321  eliotaeu  5322  csbiotag  5326  dffun2  5343  dffun4  5344  dffun5r  5345  dffun6f  5346  dffun4f  5349  sbcfung  5357  funopg  5367  fundif  5381  funinsn  5386  funcnveq  5400  fun11  5404  fununi  5405  funcnvuni  5406  imain  5419  isarep2  5424  brprcneu  5641  fv2  5643  elfv  5646  fv3  5671  relelfvdm  5680  fvmpt2  5739  ralrnmpt  5797  rexrnmpt  5798  ffnfvf  5814  f1veqaeq  5920  dff13f  5921  fliftfuns  5949  canth  5979  cbvriotavw  5992  cbvriota  5993  csbriotag  5995  acexmid  6027  oprabidlem  6059  cbvmpox  6109  cbvmpo  6110  cbvmpov  6111  mpofun  6133  abrexex2  6295  fmpoco  6390  f1o2ndf1  6402  poxp  6406  suppfnss  6435  tposoprab  6489  tfrlem3-2d  6521  tfrlemi1  6541  tfr1onlemsucfn  6549  tfr1onlemaccex  6557  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  dcdifsnid  6715  fnsnsplitdc  6716  funresdfunsndc  6717  eqerlem  6776  qliftfuns  6831  eroveu  6838  cbvixp  6927  mptelixpg  6946  idssen  6993  modom  7037  pw2f1odclem  7063  xpf1o  7073  xpmapen  7079  findcard2d  7123  fidcen  7131  eqsndc  7138  nnwetri  7151  fiintim  7166  snexxph  7192  fidcenumlemim  7194  fidcenumlemrk  7196  fidcenum  7198  supmoti  7235  isoti  7249  supisoti  7252  cnvti  7261  ordiso2  7277  ctssdccl  7353  finct  7358  infnninf  7366  nninfwlpoim  7421  nninfwlpo  7423  sspw1or2  7446  exmidontriimlem3  7481  exmidontriimlem4  7482  exmidontriim  7483  onntri13  7499  onntri51  7501  onntri3or  7506  dftap2  7513  netap  7516  2onetap  7517  2omotaplemap  7519  cc1  7527  cc2  7529  ltsopi  7583  addpipqqs  7633  mulpipqqs  7636  archpr  7906  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlemlim  7924  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdrl  7941  caucvgprprlemcbv  7950  caucvgprprlemopu  7962  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  suplocexprlemmu  7981  suplocexprlemdisj  7983  caucvgsrlembound  8057  caucvgsrlembnd  8064  suplocsrlem  8071  suplocsr  8072  peano1nnnn  8115  axcaucvglemres  8162  axpre-suploc  8165  negf1o  8604  lbreu  9168  lbinf  9171  suprubex  9174  suprlubex  9175  suprleubex  9177  1nn  9197  uzind4s  9869  uzind4s2  9870  indstr  9872  supinfneg  9874  infsupneg  9875  infregelbex  9877  eqreznegel  9893  lbzbi  9895  elpq  9928  zsupcl  10537  infssuzex  10539  infssuzledc  10540  zsupssdc  10544  exbtwnzlemex  10555  exbtwnz  10556  rebtwn2zlemstep  10558  rebtwn2z  10560  iseqovex  10766  iseqvalcbv  10767  seqvalcd  10769  seqovcd  10775  seq3f1olemqsum  10821  seq3f1olemp  10823  seq3f1oleml  10824  seqf1og  10829  seq3distr  10840  faclbnd6  11052  fimaxq  11137  wrd2ind  11353  reuccatpfxs1lem  11376  reuccatpfxs1  11377  cvg1nlemres  11608  resqrexlemsqa  11647  resqrexlemex  11648  cau3lem  11737  fclim  11917  climeu  11919  cn1lem  11937  climcau  11970  climcvg1n  11973  summodclem3  12004  summodclem2a  12005  summodclem2  12006  summodc  12007  zsumdc  12008  fsum3  12011  isumz  12013  isumss2  12017  fsumsersdc  12019  fsum3ser  12021  fsumadd  12030  fsum2dlemstep  12058  fisumcom2  12062  isumshft  12114  cvgratz  12156  mertensabs  12161  prodfdivap  12171  cbvprod  12182  prodmodclem3  12199  prodmodclem2a  12200  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodseq  12207  fprodm1s  12225  fprodp1s  12226  fprod2dlemstep  12246  fprodcom2fi  12250  fprodsplitf  12256  odd2np1lem  12496  bitsfzolem  12578  bezoutlemmain  12632  bezoutlemeu  12641  gcdmultiple  12654  rplpwr  12661  nnwofdc  12672  nnwosdc  12673  nninfctlemfo  12674  isprm5lem  12776  isprm5  12777  pw2dvdseu  12803  hashdvds  12856  eulerthlemh  12866  reumodprminv  12889  pclemub  12923  pclemdc  12924  pceu  12931  pcmptdvds  12981  1arith  13003  4sqlem2  13025  4sqlem11  13037  4sqlem12  13038  ennnfonelemg  13087  ennnfoneleminc  13095  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemrnh  13100  ennnfonelemfun  13101  ennnfonelemdm  13104  ennnfonelemr  13107  ennnfone  13109  inffinp1  13113  ctinf  13114  nninfdclemf  13133  nninfdclemp1  13134  unbendc  13138  infpn2  13140  strsetsid  13178  mgmidmo  13518  lidrididd  13528  mndinvmod  13591  insubm  13631  dfgrp3mlem  13744  mulgaddcom  13796  mulginvcom  13797  isnsg2  13853  gsumfzconstf  13992  srgmulgass  14066  islmodd  14372  lmodvsmmulgdi  14402  rmodislmodlem  14429  rmodislmod  14430  lssats2  14493  mplsubgfilemcl  14783  baspartn  14844  cnpnei  15013  txdis1cn  15072  cnmptid  15075  xmetxp  15301  cncfmptc  15390  cncfmptid  15391  dedekindeulemloc  15413  dedekindicclemloc  15422  ivthinclemlr  15431  ivthinclemur  15433  ivthinclemloc  15435  ivthdec  15438  dvmptfsum  15519  plymullem1  15542  perfectlem2  15797  lgseisenlem2  15873  lgsquadlem3  15881  lgsquad  15882  lgsquad2lem2  15884  2lgslem1a  15890  usgruspgrben  16110  umgr2edg1  16133  umgr2edgneu  16136  usgredg4  16139  usgredgreu  16140  uspgredg2vtxeu  16142  vtxedgfi  16213  vtxlpfi  16214  depindlem1  16430  depindlem2  16431  depindlem3  16432  spimd  16466  2spim  16467  ch2var  16468  bj-sbimedh  16472  bj-sbimeh  16473  cbvrald  16489  sumdc2  16500  bdth  16530  bdcdeq  16538  bdne  16552  bdreu  16554  bdcsn  16569  bdsep2  16585  bdsepnft  16586  bdsepnfALT  16588  bdbm1.3ii  16590  bj-nalset  16594  bj-zfpair2  16609  bj-bdfindes  16648  bj-nn0suc0  16649  bj-nntrans  16650  setindft  16664  setindis  16666  bdsetindis  16668  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672  strcoll2  16682  strcollnft  16683  strcollnfALT  16685  sscoll2  16687  nnti  16695  2omap  16698  nnsf  16714  peano4nninf  16715  nninfsellemqall  16724  nninfomni  16728  nnnninfen  16730  repiecef  16743  trilpolemeq1  16755  tridceq  16772  redc0  16773  reap0  16774  dceqnconst  16776  dcapnconst  16777  nconstwlpolemgt0  16780