Theorem weq 1299

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

(Instead of introducing weq 1299 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 1298. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1299 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1298. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.)

Assertion

Ref	Expression
weq	wff x = y

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1298	1 wff x = y

Syntax hints:   = wceq 1298

This theorem is referenced by:  equidqe 1314  equidq 1315  ax4sp1 1316  ax4 1318  ax9o 1480  ax9 1482  a9e 1483  equid 1484  equidALT 1485  stdpc6 1486  equcomi 1487  equcom 1488  equcoms 1489  equtr 1490  equtrr 1491  equtr2 1492  equtr2OLD 1493  equequ1 1494  equequ2 1495  elequ1 1496  elequ2 1497  ax11i 1498  ax10o 1499  ax10 1501  alequcoms 1503  nalequcoms 1504  hbae 1505  hbaes 1506  hbnae 1507  hbnaes 1508  equs3 1509  equs4 1510  equsal 1511  equsalOLD 1512  equsex 1513  dvelimfALT 1514  dral1 1515  dral2 1516  drex1 1517  drex2 1518  a4imt 1519  a4im 1520  a4ime 1521  a4imed 1522  cbv1 1523  cbv2 1524  cbv3 1525  cbv3ALT 1526  cbval 1527  cbvalOLD 1528  cbvex 1529  chvar 1530  equvini 1531  equviniOLD 1532  hbequid2 1533  sbimi 1537  drsb1 1539  sb1 1540  sb2 1541  sbequ1 1542  sbequ2 1543  sbequ12 1545  sbequ12r 1546  sbequ12rOLD 1547  sbequ12a 1548  sbid 1549  stdpc4 1550  sbf 1551  sb6xOLD 1554  hbs1fOLD 1556  sbequ5 1557  sbequ6 1558  sbtOLD 1560  equsb1 1561  equsb2 1562  sbied 1563  sbiedOLD 1564  sbie 1565  equs5a 1566  equs5e 1567  sb4a 1568  equs45f 1569  sb6f 1570  sb5f 1571  sb4e 1572  hbsb2a 1573  hbsb2e 1574  aev 1577  aevOLD 1578  ax16 1579  ax17eq 1581  dveeq2 1582  dveeq2ALT 1583  ax11v2 1585  ax11a2 1586  ax11 1589  ax11b 1590  equs5 1591  sb3 1592  sb4 1593  sb4b 1594  dfsb2 1595  dfsb3 1596  hbsb2 1597  sbequi 1598  sbequ 1599  sbn 1601  sbi1 1602  sbequ8 1618  hbsb4 1620  hbsb4t 1621  hbsb4tOLD 1622  dvelimf 1623  dvelimdf 1624  sbco 1625  sbidm 1627  sbidmOLD 1628  sbco2 1629  sbco3 1631  sbcom 1632  sb5rf 1633  sb5rfOLD 1634  sb6rf 1635  sb6rfOLD 1636  sb9i 1640  ax11v 1642  sb56 1643  sb6 1644  sb5 1645  equid1 1646  ax16i 1647  a4v 1649  a4eiv 1651  equvin 1652  a16g 1653  a16gOLD 1654  a16gb 1655  cbval2 1698  cbvex2 1699  cbvaldOLD 1703  cbvexd 1704  cbvex4v 1705  cleljust 1713  equsb3lemOLD 1716  equsb3 1717  elsb3 1718  elsb3OLD 1719  elsb4 1720  elsb4OLD 1721  hbs1 1722  hbsb 1723  sbcom2 1724  2sb5 1725  2sb6 1726  sb6a 1727  2sb5rf 1728  2sb6rf 1729  dfsb7 1730  sb7f 1731  sb7fOLD 1732  sb10f 1733  sbelx 1735  sbel2x 1736  sbal1 1737  sbal 1738  exsb 1741  2exsb 1742  dvelimALT 1744  dveeq1 1745  dveeq1ALT 1746  sbal2 1749  ax15 1750  ax17el 1752  ax11eq 1754  ax11el 1755  ax11f 1756  ax11indn 1757  ax11indi 1758  ax11indalem 1759  ax11inda2ALT 1760  ax11inda2 1761  ax11inda 1762  a12stdy1 1763  a12stdy2 1764  a12stdy3 1765  a12stdy4 1766  a12lem1 1767  a12lem2 1768  a12study 1769  a12studyALT 1770  eujustALT 1774  euf 1777  eubid 1778  eubii 1780  hbeu1 1781  hbeu 1782  sb8euOLD 1784  eu1 1786  mo 1787  euex 1788  euexOLD 1789  eumo0 1790  eu2 1791  eu3 1792  mo2 1795  mo3 1797  mo4f 1798  mobii 1801  eu5 1805  eu4 1806  immo 1813  moimv 1815  moanim 1826  mopick 1833  2mo 1851  2mos 1852  2eu4 1856  2eu5 1857  2eu6 1858  euequ1 1861  exists1 1862  exists2OLD 1864  eufnfv 4771  sbcoreleleq 5830  tratrb 5831  ordelordaxr 5833  axextprim 13785  axrepprim 13786  axpowprim 13788  axacprim 13791  untsucf 13798  untangtr 13802  fundmpss 13836  mpt2fun 13843  setinds 13844  dfon2lem1 13849  dfon2lem3 13851  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  dfon2 13858  axextdfeq 13864  ax13dfeq 13865  axextdist 13866  axext4dist 13867  distel 13870  cbvsetlike 13892  preddowncl 13907  tfisg 13912  tz6.26 13913  trcltr 13936  frmin 13938  frinsg 13941  xporderlem 13948  poxp 13949  soxp 13950  frxp 13951  poseq 13954  soseq 13955  wfr3g 13956  wfrlem1 13957  wfrlem5 13961  wfrlem10 13966  wfrlem11 13967  wfrlem14 13970  wfrlem15 13971  wfr2 13974  tfr3ALT 13979  frr3g 13980  sltval2 13997  axsltsolem1 14006  axbday 14012  axdenselem5 14023  nocvxminlem 14028  nocvxmin 14029  axfelem5 14035  axfelem8 14038  axfelem9 14039  axfelem10 14040  axfelem12 14042  axfelem15 14045  axfelem16 14046  brtxp 14067  idsset 14070  dfon3 14072  fnbigcup 14075  unisym1 14247  ref4w 14370  srefwref 14373  injrec 14461  mapmapmap 14486  injsurinj 14487  mxlelt2 14606  mxlelt 14607  mnlelt2 14608  ismxl2 14609  ismnl2 14610  mnlmxl2 14611  dfdir2 14639  hbprod 14660  cbvprodi 14662  fprod1s 14677  fprodp1s 14682  mgmlion 14697  clfsebs 14707  fincmpzer 14711  fprodadd 14713  fprodneg 14741  usptoplem 14917  istopx 14918  prtoptop 14919  usptop 14920  fbaslim2 14936  iscnp3 14946  pm13.193 16375  ipo0 16426  glbcon 17028  glbconx 17029  pmapglbx 17251  pmapglb 17252  paddasslem5 17285  paddasslem12 17292  paddasslem14 17294  polval2 17319  pexmidlem1 17378

Copyright terms: Public domain