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

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

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

Proof of Theorem weq
StepHypRef Expression
1 wceq 1322 1
Colors of variables: wff set class
Syntax hints:   wceq 1322
This theorem is referenced by:  alequcoms  1339  equidqe  1354  equidqeOLD  1355  ax4sp1  1356  equid  1478  stdpc6  1479  equcomi  1480  equcom  1481  equcoms  1482  equtr  1483  equtrr  1484  equtr2  1485  equequ1  1486  equequ2  1487  elequ1  1488  elequ2  1489  ax11i  1490  ax10o  1491  ax10  1493  nfae  1495  hbaes  1496  hbnae  1497  nfnae  1498  hbnaes  1499  equsal  1502  dral1  1505  dral2  1506  drex2  1507  drnf1  1508  drnf2  1509  a4imt  1510  a4im  1511  a4imed  1513  cbv1  1514  cbv2  1515  cbv3h  1516  cbv3ALT  1517  cbvalh  1518  chvar  1522  sbimi  1532  sb1  1534  sb2  1535  sbequ1  1536  sbequ2  1537  sbequ12  1539  sbequ12r  1540  sbequ12a  1541  sbid  1542  stdpc4  1543  sbh  1544  sbequ5  1550  sbequ6  1551  equsb1  1553  equsb2  1554  sbiedh  1555  sbieh  1557  equs5a  1559  drsb1  1564  exdistrf  1565  sb4a  1566  equs45f  1567  sb6f  1568  sb5f  1569  sb4e  1570  hbsb2a  1571  hbsb2e  1572  aev  1577  ax16  1578  dveeq2  1580  dveeq2or  1581  ax11v2  1585  ax11a2  1586  ax11b  1591  equs5  1594  equs5or  1595  sb3  1596  sb4  1597  sb4or  1598  sb4b  1599  sb4bor  1600  hbsb2  1601  nfsb2or  1602  sbequi  1604  sbequ  1605  a4sbim  1608  sbequ8  1611  sbidm  1614  sb5rf  1615  sb6rf  1616  ax16i  1619  a4v  1621  a4eiv  1623  equvin  1624  a16g  1625  a16gb  1626  a16nf  1627  sb56  1645  sb6  1646  sb5  1647  sborv  1650  sbi2v  1652  cbval2  1674  cbvex2  1675  cbvex4v  1680  cleljust  1687  nfsbxy  1693  nfsbxyt  1694  equsb3  1700  sbco  1717  sbcocom  1719  sbcomxyyz  1721  elsb3  1727  elsb4  1728  sb9v  1729  2sb5  1733  2sb6  1734  sbcom2v  1735  sb6a  1739  2sb5rf  1740  2sb6rf  1741  dfsb7  1742  sb7f  1743  sb10f  1746  sbel2x  1749  sbal1yz  1752  sbal1  1753  exsb  1757  2exsb  1758  dvelimALT  1759  dvelimfv  1760  hbsb4t  1762  dvelimf  1764  dvelimdf  1765  dvelimor  1767  dveeq1  1768  sbal2  1771  axext3  1774  axext4  1775  cleqh  1887  cbvab  1908  sbab  1912  nfcjust  1914  drnfc1  1942  drnfc2  1943  dvelimdc  1945  dvelimc  1946  nfcvf  1947  eujustALT  1991  euf  1994  eubid  1995  eubii  1997  hbeu1  1998  hbeu  1999  eu1  2003  mo  2004  euex  2005  eumo0  2006  eu2  2007  eu3  2008  mo2  2011  mo3  2013  mo4f  2014  mobii  2017  eu5  2021  eu4  2022  immo  2029  moimv  2031  moanim  2039  mopick  2045  2mo  2061  2mos  2062  2eu4  2066  2eu5  2067  2eu6  2068  euequ1  2071  exists1  2072  dfsb2  2097  dfsb3  2098
  Copyright terms: Public domain W3C validator