Theorem weq 1551

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

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

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1397	1 wff 𝑥 = 𝑦

Syntax hints:   = wceq 1397

This theorem is referenced by:  alequcoms  1564  equidqe  1580  ax4sp1  1581  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  cbvabw  2354  cbvab  2355  sbab  2359  nfcjust  2362  drnfc1  2391  drnfc2  2392  nfabdw  2393  dvelimdc  2395  dvelimc  2396  nfcvf  2397  cbvrmow  2716  cbvralfw  2756  cbvrexfw  2757  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvralvw  2771  cbvrexvw  2772  cbvreuvw  2773  cbvraldva2  2774  cbvrexdva2  2775  cbvraldva  2776  cbvrexdva  2777  cbvral2vw  2778  cbvrex2vw  2779  cbvral2v  2780  cbvrex2v  2781  cbvral3v  2782  sbralie  2785  cbvrab  2800  vjust  2803  vex  2805  rr19.3v  2945  rr19.28v  2946  ralab2  2970  rexab2  2972  reu2  2994  reu6  2995  reu3  2996  rmo4  2999  reu4  3000  reu7  3001  reu8  3002  rmo3f  3003  rmo4f  3004  cdeqi  3016  cdeqri  3017  cdeqth  3018  cdeqnot  3019  cdeqal  3020  cdeqab  3021  cdeqim  3024  cdeqcv  3025  cdeqeq  3026  cdeqel  3027  nfccdeq  3029  sbsbc  3035  sbc8g  3039  sbcco2  3054  sbc5  3055  sbcralt  3108  sbcralg  3110  sbcreug  3112  reu8nf  3113  rmo3  3124  cbvcsbw  3131  cbvcsb  3132  csbcow  3138  sbcel12g  3142  sbceqg  3143  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  difjust  3201  unjust  3203  injust  3205  dfss2f  3218  dfdif3  3317  dfnul3  3497  dfif3  3619  rabsnifsb  3737  preq12bg  3856  eluniab  3905  elintab  3939  int0  3942  dfiunv2  4006  cbviun  4007  cbviin  4008  cbvdisj  4074  invdisjrab  4082  disjiun  4083  sndisj  4084  sbcbrg  4143  cbvmptf  4183  cbvmpt  4184  axsep2  4208  bm1.3ii  4210  nalset  4219  zfpow  4265  el  4268  dtruarb  4281  copsexg  4336  opelopabsb  4354  swopo  4403  pofun  4409  issod  4416  frind  4449  zfun  4531  ruv  4648  dtru  4658  dcextest  4679  tfisi  4685  findes  4701  relop  4880  dfdmf  4924  dfrnf  4973  resiexg  5058  dfres2  5065  opabresid  5066  mptresid  5067  imai  5092  issref  5119  intasym  5121  cnvi  5141  rnxpid  5171  cnvpom  5279  nfiota1  5288  cbviota  5291  sb8iota  5294  iotaval  5298  iotanul  5302  iota4  5306  eliota  5314  eliotaeu  5315  csbiotag  5319  dffun2  5336  dffun4  5337  dffun5r  5338  dffun6f  5339  dffun4f  5342  sbcfung  5350  funopg  5360  fundif  5374  funinsn  5379  funcnveq  5393  fun11  5397  fununi  5398  funcnvuni  5399  imain  5412  isarep2  5417  brprcneu  5632  fv2  5634  elfv  5637  fv3  5662  relelfvdm  5671  fvmpt2  5730  ralrnmpt  5789  rexrnmpt  5790  ffnfvf  5806  f1veqaeq  5910  dff13f  5911  fliftfuns  5939  canth  5969  cbvriotavw  5982  cbvriota  5983  csbriotag  5985  acexmid  6017  oprabidlem  6049  cbvmpox  6099  cbvmpo  6100  cbvmpov  6101  mpofun  6123  abrexex2  6286  fmpoco  6381  f1o2ndf1  6393  poxp  6397  tposoprab  6446  tfrlem3-2d  6478  tfrlemi1  6498  tfr1onlemsucfn  6506  tfr1onlemaccex  6514  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  dcdifsnid  6672  fnsnsplitdc  6673  funresdfunsndc  6674  eqerlem  6733  qliftfuns  6788  eroveu  6795  cbvixp  6884  mptelixpg  6903  idssen  6950  modom  6994  pw2f1odclem  7020  xpf1o  7030  xpmapen  7036  findcard2d  7080  fidcen  7088  eqsndc  7095  nnwetri  7108  fiintim  7123  snexxph  7149  fidcenumlemim  7151  fidcenumlemrk  7153  fidcenum  7155  supmoti  7192  isoti  7206  supisoti  7209  cnvti  7218  ordiso2  7234  ctssdccl  7310  finct  7315  infnninf  7323  nninfwlpoim  7378  nninfwlpo  7380  sspw1or2  7403  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  onntri13  7456  onntri51  7458  onntri3or  7463  dftap2  7470  netap  7473  2onetap  7474  2omotaplemap  7476  cc1  7484  cc2  7486  ltsopi  7540  addpipqqs  7590  mulpipqqs  7593  archpr  7863  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlemlim  7881  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgprprlemcbv  7907  caucvgprprlemopu  7919  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  suplocexprlemmu  7938  suplocexprlemdisj  7940  caucvgsrlembound  8014  caucvgsrlembnd  8021  suplocsrlem  8028  suplocsr  8029  peano1nnnn  8072  axcaucvglemres  8119  axpre-suploc  8122  negf1o  8561  lbreu  9125  lbinf  9128  suprubex  9131  suprlubex  9132  suprleubex  9134  1nn  9154  uzind4s  9824  uzind4s2  9825  indstr  9827  supinfneg  9829  infsupneg  9830  infregelbex  9832  eqreznegel  9848  lbzbi  9850  elpq  9883  zsupcl  10492  infssuzex  10494  infssuzledc  10495  zsupssdc  10499  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  iseqovex  10721  iseqvalcbv  10722  seqvalcd  10724  seqovcd  10730  seq3f1olemqsum  10776  seq3f1olemp  10778  seq3f1oleml  10779  seqf1og  10784  seq3distr  10795  faclbnd6  11007  fimaxq  11092  wrd2ind  11308  reuccatpfxs1lem  11331  reuccatpfxs1  11332  cvg1nlemres  11550  resqrexlemsqa  11589  resqrexlemex  11590  cau3lem  11679  fclim  11859  climeu  11861  cn1lem  11879  climcau  11912  climcvg1n  11915  summodclem3  11946  summodclem2a  11947  summodclem2  11948  summodc  11949  zsumdc  11950  fsum3  11953  isumz  11955  isumss2  11959  fsumsersdc  11961  fsum3ser  11963  fsumadd  11972  fsum2dlemstep  12000  fisumcom2  12004  isumshft  12056  cvgratz  12098  mertensabs  12103  prodfdivap  12113  cbvprod  12124  prodmodclem3  12141  prodmodclem2a  12142  prodmodclem2  12143  prodmodc  12144  zproddc  12145  fprodseq  12149  fprodm1s  12167  fprodp1s  12168  fprod2dlemstep  12188  fprodcom2fi  12192  fprodsplitf  12198  odd2np1lem  12438  bitsfzolem  12520  bezoutlemmain  12574  bezoutlemeu  12583  gcdmultiple  12596  rplpwr  12603  nnwofdc  12614  nnwosdc  12615  nninfctlemfo  12616  isprm5lem  12718  isprm5  12719  pw2dvdseu  12745  hashdvds  12798  eulerthlemh  12808  reumodprminv  12831  pclemub  12865  pclemdc  12866  pceu  12873  pcmptdvds  12923  1arith  12945  4sqlem2  12967  4sqlem11  12979  4sqlem12  12980  ennnfonelemg  13029  ennnfoneleminc  13037  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemrnh  13042  ennnfonelemfun  13043  ennnfonelemdm  13046  ennnfonelemr  13049  ennnfone  13051  inffinp1  13055  ctinf  13056  nninfdclemf  13075  nninfdclemp1  13076  unbendc  13080  infpn2  13082  strsetsid  13120  mgmidmo  13460  lidrididd  13470  mndinvmod  13533  insubm  13573  dfgrp3mlem  13686  mulgaddcom  13738  mulginvcom  13739  isnsg2  13795  gsumfzconstf  13934  srgmulgass  14008  islmodd  14313  lmodvsmmulgdi  14343  rmodislmodlem  14370  rmodislmod  14371  lssats2  14434  mplsubgfilemcl  14719  baspartn  14780  cnpnei  14949  txdis1cn  15008  cnmptid  15011  xmetxp  15237  cncfmptc  15326  cncfmptid  15327  dedekindeulemloc  15349  dedekindicclemloc  15358  ivthinclemlr  15367  ivthinclemur  15369  ivthinclemloc  15371  ivthdec  15374  dvmptfsum  15455  plymullem1  15478  perfectlem2  15730  lgseisenlem2  15806  lgsquadlem3  15814  lgsquad  15815  lgsquad2lem2  15817  2lgslem1a  15823  usgruspgrben  16043  umgr2edg1  16066  umgr2edgneu  16069  usgredg4  16072  usgredgreu  16073  uspgredg2vtxeu  16075  vtxedgfi  16146  vtxlpfi  16147  depindlem1  16351  depindlem2  16352  depindlem3  16353  spimd  16387  2spim  16388  ch2var  16389  bj-sbimedh  16393  bj-sbimeh  16394  cbvrald  16410  sumdc2  16421  bdth  16452  bdcdeq  16460  bdne  16474  bdreu  16476  bdcsn  16491  bdsep2  16507  bdsepnft  16508  bdsepnfALT  16510  bdbm1.3ii  16512  bj-nalset  16516  bj-zfpair2  16531  bj-bdfindes  16570  bj-nn0suc0  16571  bj-nntrans  16572  setindft  16586  setindis  16588  bdsetindis  16590  bj-inf2vnlem3  16593  bj-inf2vnlem4  16594  strcoll2  16604  strcollnft  16605  strcollnfALT  16607  sscoll2  16609  nnti  16617  2omap  16620  nnsf  16633  peano4nninf  16634  nninfsellemqall  16643  nninfomni  16647  nnnninfen  16649  trilpolemeq1  16670  tridceq  16686  redc0  16687  reap0  16688  dceqnconst  16690  dcapnconst  16691  nconstwlpolemgt0  16694