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

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

(Instead of introducing weq 1373 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 1228. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1373 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1228. 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 1228 1 wff x = y
Colors of variables: wff set class
Syntax hints:   = wceq 1228
This theorem is referenced by:  alequcoms  1390  equidqe  1406  equidqeOLD  1407  ax4sp1  1408  equid  1571  nfequid  1572  stdpc6  1573  equcomi  1574  equcom  1575  equcoms  1576  equtr  1577  equtrr  1578  equtr2  1579  equequ1  1580  equequ2  1581  elequ1  1582  elequ2  1583  ax11i  1584  ax10o  1585  ax10  1587  nfae  1589  hbaes  1590  hbnae  1591  nfnae  1592  hbnaes  1593  equsalh  1596  equsal  1597  dral1  1600  dral2  1601  drex2  1602  drnf1  1603  drnf2  1604  spimth  1605  spimh  1607  spimed  1610  cbv1  1614  cbv1h  1615  cbv2h  1616  cbvalh  1618  chvar  1622  sbimi  1629  sb1  1631  sb2  1632  sbequ1  1633  sbequ2  1634  sbequ12  1636  sbequ12r  1637  sbequ12a  1638  sbid  1639  stdpc4  1640  sbh  1641  sb6x  1644  sbequ5  1647  sbequ6  1648  equsb1  1650  equsb2  1651  sbiedh  1652  sbiedv  1654  sbieh  1655  equs5a  1657  drsb1  1662  exdistrfor  1663  sb4a  1664  equs45f  1665  sb6f  1666  sb5f  1667  sb4e  1668  hbsb2a  1669  hbsb2e  1670  sbcof2  1673  aev  1675  ax16  1676  dveeq2  1678  dveeq2or  1679  ax11v2  1683  ax11a2  1684  ax11b  1689  equs5  1692  equs5or  1693  sb3  1694  sb4  1695  sb4or  1696  sb4b  1697  sb4bor  1698  hbsb2  1699  nfsb2or  1700  sbequi  1702  sbequ  1703  drsb2  1704  spsbe  1705  spsbim  1706  sbequ8  1709  sbidm  1713  sb5rf  1714  sb6rf  1715  ax16i  1720  spv  1722  speiv  1724  equvin  1725  a16g  1726  a16gb  1727  a16nf  1728  sb56  1747  sb6  1748  sb5  1749  sbnv  1750  sbanv  1751  sborv  1752  sbi1v  1753  sbi2v  1754  cbval2  1778  cbvex2  1779  cbvaldva  1785  cbvexdva  1786  cbvex4v  1787  cleljust  1795  hbs1  1796  hbsbv  1799  nfsbxy  1800  nfsbxyt  1801  equsb3  1807  sbco  1824  sbcocom  1826  sbcomxyyz  1828  elsb3  1834  elsb4  1835  sb9v  1836  2sb5  1841  2sb6  1842  sbcom2v  1843  sb6a  1846  2sb5rf  1847  2sb6rf  1848  dfsb7  1849  sb7f  1850  sb7af  1851  sb10f  1853  sbel2x  1856  sbalyz  1857  sbal1yz  1859  sbal1  1860  sbexyz  1861  exsb  1866  2exsb  1867  dvelimALT  1868  dvelimfv  1869  hbsb4t  1871  nfsb4t  1872  dvelimf  1873  dvelimdf  1874  dvelimor  1876  dveeq1  1877  sbal2  1880  euf  1887  eubidh  1888  eubid  1889  hbeu1  1892  nfeu1  1893  sb8eu  1895  nfeuv  1900  sb8euh  1905  eu1  1907  mo2n  1910  euex  1912  eumo0  1913  mo23  1923  mor  1924  modc  1925  eu2  1926  eu3h  1927  mo2r  1934  mo3h  1935  mo2dc  1937  mo4f  1942  eu4  1944  moim  1946  moimv  1948  moanim  1956  mopick  1960  2eu4  1975  euequ1  1977  exists1  1978  axext3  2005  axext4  2006  bm1.1  2007  cleqh  2119  cbvab  2142  sbab  2146  nfcjust  2148  drnfc1  2176  drnfc2  2177  dvelimdc  2179  dvelimc  2180  nfcvf  2181  cbvralf  2505  cbvrexf  2506  cbvreu  2509  cbvraldva2  2515  cbvrexdva2  2516  cbvraldva  2517  cbvrexdva  2518  cbvral2v  2519  cbvrex2v  2520  cbvral3v  2521  cbvrab  2533  vjust  2536  vex  2538  rr19.3v  2659  rr19.28v  2660  ralab2  2682  rexab2  2684  reu2  2706  reu6  2707  reu3  2708  rmo4  2711  reu4  2712  reu7  2713  reu8  2714  cdeqi  2726  cdeqri  2727  cdeqth  2728  cdeqnot  2729  cdeqal  2730  cdeqab  2731  cdeqim  2734  cdeqcv  2735  cdeqeq  2736  cdeqel  2737  nfccdeq  2739  sbsbc  2745  sbc8g  2748  sbcco2  2763  sbc5  2764  sbcralt  2811  sbcralg  2813  sbcrexg  2814  sbcreug  2815  rmo3  2826  cbvcsb  2833  sbcel12g  2842  sbceqg  2843  cbvralcsf  2885  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  difjust  2896  unjust  2898  injust  2900  dfss2f  2913  dfnul3  3204  dfif3  3320  preq12bg  3518  eluniab  3566  elintab  3600  int0  3603  dfiunv2  3667  cbviun  3668  cbviin  3669  cbvdisj  3729  sndisj  3734  sbcbrg  3787  cbvmpt  3825  axsep2  3850  bm1.3ii  3852  nalset  3861  zfpow  3902  el  3905  dtruarb  3916  copsexg  3955  opelopabsb  3971  swopo  4017  pofun  4023  issod  4030  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  5674  fmpt2co  5760  f1o2ndf1  5772  poxp  5775  tposoprab  5817  tfrlem3-2d  5850  tfrlemi1  5867  eqerlem  6048  qliftfuns  6101  eroveu  6108  ltsopi  6180  addpipqqs  6229  mulpipqqs  6232  spimd  7012  2spim  7013  ch2var  7014  bj-sbimedh  7018  bj-sbimeh  7019  cbvrald  7034  bdth  7058  bdcdeq  7066  bdne  7080  bdreu  7082  bdcsn  7097  bdsep2  7112  bdsepnft  7113  bdsepnfALT  7115  bdbm1.3ii  7117  bj-nalset  7118  bj-zfpair2  7133  bj-bdfindes  7171  bj-nn0suc0  7172  bj-nntrans  7173  setindft  7183  setindis  7185  bdsetindis  7187  bj-inf2vnlem3  7190  bj-inf2vnlem4  7191  strcoll2  7201  strcollnft  7202  strcollnfALT  7204  sscoll2  7206
  Copyright terms: Public domain W3C validator