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

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

(Instead of introducing weq 1379 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 1233. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1379 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1233. 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
StepHypRef Expression
1 wceq 1233 1 wff x = y
Colors of variables: wff set class
Syntax hints:   = wceq 1233
This theorem is referenced by:  alequcoms  1396  equidqe  1412  equidqeOLD  1413  ax4sp1  1414  equid  1577  nfequid  1578  stdpc6  1579  equcomi  1580  equcom  1581  equcoms  1582  equtr  1583  equtrr  1584  equtr2  1585  equequ1  1586  equequ2  1587  elequ1  1588  elequ2  1589  ax11i  1590  ax10o  1591  ax10  1593  nfae  1595  hbaes  1596  hbnae  1597  nfnae  1598  hbnaes  1599  equsalh  1602  equsal  1603  dral1  1606  dral2  1607  drex2  1608  drnf1  1609  drnf2  1610  spimth  1611  spimh  1613  spimed  1616  cbv1  1620  cbv1h  1621  cbv2h  1622  cbvalh  1624  chvar  1628  sbimi  1635  sb1  1637  sb2  1638  sbequ1  1639  sbequ2  1640  sbequ12  1642  sbequ12r  1643  sbequ12a  1644  sbid  1645  stdpc4  1646  sbh  1647  sb6x  1650  sbequ5  1653  sbequ6  1654  equsb1  1656  equsb2  1657  sbiedh  1658  sbiedv  1660  sbieh  1661  equs5a  1663  drsb1  1668  exdistrfor  1669  sb4a  1670  equs45f  1671  sb6f  1672  sb5f  1673  sb4e  1674  hbsb2a  1675  hbsb2e  1676  sbcof2  1679  aev  1681  ax16  1682  dveeq2  1684  dveeq2or  1685  ax11v2  1689  ax11a2  1690  ax11b  1695  equs5  1698  equs5or  1699  sb3  1700  sb4  1701  sb4or  1702  sb4b  1703  sb4bor  1704  hbsb2  1705  nfsb2or  1706  sbequi  1708  sbequ  1709  drsb2  1710  spsbe  1711  spsbim  1712  sbequ8  1715  sbidm  1719  sb5rf  1720  sb6rf  1721  ax16i  1726  spv  1728  speiv  1730  equvin  1731  a16g  1732  a16gb  1733  a16nf  1734  sb56  1753  sb6  1754  sb5  1755  sbnv  1756  sbanv  1757  sborv  1758  sbi1v  1759  sbi2v  1760  cbval2  1783  cbvex2  1784  cbvaldva  1790  cbvexdva  1791  cbvex4v  1792  cleljust  1799  hbs1  1800  hbsbv  1803  nfsbxy  1804  nfsbxyt  1805  equsb3  1811  sbco  1828  sbcocom  1830  sbcomxyyz  1832  elsb3  1838  elsb4  1839  sb9v  1840  2sb5  1845  2sb6  1846  sbcom2v  1847  sb6a  1850  2sb5rf  1851  2sb6rf  1852  dfsb7  1853  sb7f  1854  sb7af  1855  sb10f  1857  sbel2x  1860  sbalyz  1861  sbal1yz  1863  sbal1  1864  sbexyz  1865  exsb  1870  2exsb  1871  dvelimALT  1872  dvelimfv  1873  hbsb4t  1875  nfsb4t  1876  dvelimf  1877  dvelimdf  1878  dvelimor  1880  dveeq1  1881  sbal2  1884  euf  1891  eubidh  1892  eubid  1893  hbeu1  1896  nfeu1  1897  sb8eu  1899  nfeuv  1904  sb8euh  1909  eu1  1911  mo2n  1914  euex  1916  eumo0  1917  mo23  1927  mor  1928  modc  1929  eu2  1930  eu3h  1931  mo2r  1938  mo3h  1939  mo2dc  1941  mo4f  1946  eu4  1948  moim  1950  moimv  1952  moanim  1960  mopick  1964  2eu4  1979  euequ1  1981  exists1  1982  axext3  2009  axext4  2010  bm1.1  2011  cleqh  2123  cbvab  2146  sbab  2150  nfcjust  2152  drnfc1  2180  drnfc2  2181  dvelimdc  2183  dvelimc  2184  nfcvf  2185  cbvralf  2507  cbvrexf  2508  cbvreu  2511  cbvraldva2  2517  cbvrexdva2  2518  cbvraldva  2519  cbvrexdva  2520  cbvral2v  2521  cbvrex2v  2522  cbvral3v  2523  cbvrab  2535  vjust  2538  vex  2540  rr19.3v  2661  rr19.28v  2662  ralab2  2684  rexab2  2686  reu2  2708  reu6  2709  reu3  2710  rmo4  2713  reu4  2714  reu7  2715  reu8  2716  cdeqi  2728  cdeqri  2729  cdeqth  2730  cdeqnot  2731  cdeqal  2732  cdeqab  2733  cdeqim  2736  cdeqcv  2737  cdeqeq  2738  cdeqel  2739  nfccdeq  2741  sbsbc  2747  sbc8g  2750  sbcco2  2765  sbc5  2766  sbcralt  2813  sbcralg  2815  sbcrexg  2816  sbcreug  2817  rmo3  2828  cbvcsb  2835  sbcel12g  2844  sbceqg  2845  cbvralcsf  2887  cbvrexcsf  2888  cbvreucsf  2889  cbvrabcsf  2890  difjust  2898  unjust  2900  injust  2902  dfss2f  2915  dfnul3  3206  dfif3  3322  preq12bg  3520  eluniab  3568  elintab  3602  int0  3605  dfiunv2  3669  cbviun  3670  cbviin  3671  cbvdisj  3731  sndisj  3736  sbcbrg  3789  cbvmpt  3827  axsep2  3852  bm1.3ii  3854  nalset  3863  zfpow  3904  el  3907  dtruarb  3918  copsexg  3957  opelopabsb  3973  swopo  4019  pofun  4025  issod  4032  zfun  4121  ruv  4212  dtru  4222  tfisi  4237  findes  4253  relop  4413  dfdmf  4455  dfrnf  4502  resiexg  4580  dfres2  4585  opabresid  4586  mptresid  4587  imai  4608  issref  4634  intasym  4636  cnvi  4655  rnxpid  4682  cnvpom  4787  nfiota1  4796  cbviota  4799  sb8iota  4801  iotaval  4805  iotanul  4809  iota4  4812  csbiotag  4822  dffun2  4839  dffun4  4840  dffun6f  4841  dffun4f  4844  sbcfung  4851  funcnveq  4888  fun11  4892  fununi  4893  funcnvuni  4894  imain  4907  isarep2  4912  brprcneu  5096  fv2  5098  elfv  5101  fv3  5122  relelfvdm  5130  fvmpt2  5179  ralrnmpt  5234  rexrnmpt  5235  ffnfvf  5249  f1veqaeq  5333  dff13f  5334  fliftfuns  5363  cbvriota  5402  csbriotag  5404  acexmid  5435  oprabidlem  5460  cbvmpt2x  5505  cbvmpt2  5506  cbvmpt2v  5507  mpt2fun  5526  abrexex2  5673  fmpt2co  5759  f1o2ndf1  5771  poxp  5774  tposoprab  5816  tfrlem3-2d  5847  tfrlemi1  5864  eqerlem  6042  qliftfuns  6093  eroveu  6100  ltsopi  6167  addpipqqs  6214  mulpipqqs  6217  spimd  6299  2spim  6300  ch2var  6301  bdth  6322  bdne  6341  bdreu  6343  bdcdeq  6346  bdcsn  6357  bdsep2  6368  bdsepnft  6369  bdsepnfALT  6371  bdbm1.3ii  6373  bj-zfpair2  6380  strcoll2  6395  strcollnft  6396  strcollnfALT  6398  sscoll2  6400
  Copyright terms: Public domain W3C validator