ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  weq Unicode version

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

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

Assertion
Ref Expression
weq

Proof of Theorem weq
StepHypRef Expression
1 wceq 1383 1
Colors of variables: wff set class
Syntax hints:   wceq 1383
This theorem is referenced by:  alequcoms  1400  a9wa9lem1  1404  a9wa9lem2  1405  a9wa9lem2OLD  1406  a9wa9lem3  1407  a9wa9lem8  1413  a9wa9lem8OLD  1414  a9wa9  1415  equidqe  1419  equidqeOLD  1420  equidq  1421  ax4sp1  1422  ax4  1423  equs3  1526  ax9  1559  equidALT  1560  equid1  1561  stdpc6  1563  equcomi  1564  equcom  1565  equcoms  1566  equtr  1567  equtrr  1568  equtr2  1569  equequ1  1570  equequ2  1571  elequ1  1572  elequ2  1573  ax11i  1574  ax10o  1575  ax10  1577  hbaes  1579  hbnae  1580  hbnaes  1581  equsal  1583  dvelimfALT  1585  dral1  1586  dral2  1587  drex2  1589  exdistrf  1590  a4imt  1591  a4im  1592  a4imed  1594  cbv1  1595  cbv2  1596  cbv3  1597  cbv3ALT  1598  cbval  1599  chvar  1601  sbimi  1607  drsb1  1609  sb1  1610  sb2  1611  sbequ1  1612  sbequ2  1613  sbequ12  1615  sbequ12r  1616  sbequ12a  1617  sbid  1618  stdpc4  1619  sbf  1620  sbequ5  1624  sbequ6  1625  equsb1  1627  equsb2  1628  sbied  1629  sbie  1630  equs5a  1631  sb4a  1633  equs45f  1634  sb6f  1635  sb5f  1636  sb4e  1637  hbsb2a  1638  hbsb2e  1639  aev  1642  ax16  1643  ax17eq  1645  dveeq2  1646  dveeq2ALT  1647  ax11v2  1651  ax11a2  1652  ax11  1655  ax11b  1656  equs5  1657  sb3  1658  sb4  1659  sb4b  1660  dfsb2  1661  dfsb3  1662  hbsb2  1663  sbequi  1664  sbequ  1665  sbn  1667  sbi1  1668  sbequ8  1684  hbsb4  1686  hbsb4t  1687  dvelimf  1688  dvelimdf  1689  sbco  1690  sbidm  1692  sbco2  1693  sbco3  1695  sbcom  1696  sb5rf  1697  sb6rf  1698  sb9i  1701  ax11v  1703  sb56  1704  sb6  1705  sb5  1706  ax16i  1707  a4v  1709  a4eiv  1711  equvin  1712  a16g  1713  a16gb  1714  cbval2  1757  cbvex2  1758  cbvexd  1762  cbvex4v  1763  cleljust  1770  equsb3  1772  elsb3  1773  elsb4  1774  hbs1  1775  hbsb  1778  2sb5  1780  2sb6  1781  sbcom2  1782  sb6a  1784  2sb5rf  1785  2sb6rf  1786  dfsb7  1787  sb7f  1788  sb10f  1789  sbelx  1791  sbel2x  1792  sbal1  1793  sbal  1794  exsb  1797  2exsb  1798  dvelimALT  1800  dveeq1  1801  dveeq1ALT  1802  sbal2  1805  ax15  1806  ax17el  1808  ax11eq  1810  ax11el  1811  ax11f  1812  ax11indn  1813  ax11indi  1814  ax11indalem  1815  ax11inda2ALT  1816  ax11inda2  1817  ax11inda  1818  a12stdy1  1819  a12stdy2  1820  a12stdy3  1821  a12stdy4  1822  a12lem1  1823  a12lem2  1824  a12study  1825  a12studyALT  1826  a12study3  1828  eujustALT  1832  euf  1835  eubid  1836  eubii  1838  hbeu1  1839  hbeu  1840  eu1  1844  mo  1845  euex  1846  eumo0  1847  eu2  1848  eu3  1849  mo2  1852  mo3  1854  mo4f  1855  mobii  1858  eu5  1862  eu4  1863  immo  1870  moimv  1872  moanim  1880  mopick  1886  2mo  1902  2mos  1903  2eu4  1907  2eu5  1908  2eu6  1909  euequ1  1912  exists1  1913
  Copyright terms: Public domain W3C validator