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

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

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

Proof of Theorem weq
StepHypRef Expression
1 wceq 1243 1 wff 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:   = wceq 1243
This theorem is referenced by:  alequcoms  1409  equidqe  1425  ax4sp1  1426  equid  1589  nfequid  1590  stdpc6  1591  equcomi  1592  equcom  1593  equcoms  1594  equtr  1595  equtrr  1596  equtr2  1597  equequ1  1598  equequ2  1599  elequ1  1600  elequ2  1601  ax11i  1602  ax10o  1603  ax10  1605  nfae  1607  hbaes  1608  hbnae  1609  nfnae  1610  hbnaes  1611  equsalh  1614  equsal  1615  dral1  1618  dral2  1619  drex2  1620  drnf1  1621  drnf2  1622  spimth  1623  spimh  1625  spimed  1628  cbv1  1632  cbv1h  1633  cbv2h  1634  cbvalh  1636  chvar  1640  sbimi  1647  sb1  1649  sb2  1650  sbequ1  1651  sbequ2  1652  sbequ12  1654  sbequ12r  1655  sbequ12a  1656  sbid  1657  stdpc4  1658  sbh  1659  sb6x  1662  sbequ5  1665  sbequ6  1666  equsb1  1668  equsb2  1669  sbiedh  1670  sbiedv  1672  sbieh  1673  equs5a  1675  drsb1  1680  exdistrfor  1681  sb4a  1682  equs45f  1683  sb6f  1684  sb5f  1685  sb4e  1686  hbsb2a  1687  hbsb2e  1688  sbcof2  1691  aev  1693  ax16  1694  dveeq2  1696  dveeq2or  1697  ax11v2  1701  ax11a2  1702  ax11b  1707  equs5  1710  equs5or  1711  sb3  1712  sb4  1713  sb4or  1714  sb4b  1715  sb4bor  1716  hbsb2  1717  nfsb2or  1718  sbequi  1720  sbequ  1721  drsb2  1722  spsbe  1723  spsbim  1724  sbequ8  1727  sbidm  1731  sb5rf  1732  sb6rf  1733  ax16i  1738  spv  1740  speiv  1742  equvin  1743  a16g  1744  a16gb  1745  a16nf  1746  sb56  1765  sb6  1766  sb5  1767  sbnv  1768  sbanv  1769  sborv  1770  sbi1v  1771  sbi2v  1772  cbval2  1796  cbvex2  1797  cbvaldva  1803  cbvexdva  1804  cbvex4v  1805  cleljust  1813  hbs1  1814  hbsbv  1817  nfsbxy  1818  nfsbxyt  1819  equsb3  1825  sbco  1842  sbcocom  1844  sbcomxyyz  1846  elsb3  1852  elsb4  1853  sb9v  1854  2sb5  1859  2sb6  1860  sbcom2v  1861  sb6a  1864  2sb5rf  1865  2sb6rf  1866  dfsb7  1867  sb7f  1868  sb7af  1869  sb10f  1871  sbel2x  1874  sbalyz  1875  sbal1yz  1877  sbal1  1878  sbexyz  1879  exsb  1884  2exsb  1885  dvelimALT  1886  dvelimfv  1887  hbsb4t  1889  nfsb4t  1890  dvelimf  1891  dvelimdf  1892  dvelimor  1894  dveeq1  1895  sbal2  1898  euf  1905  eubidh  1906  eubid  1907  hbeu1  1910  nfeu1  1911  sb8eu  1913  nfeuv  1918  sb8euh  1923  eu1  1925  mo2n  1928  euex  1930  eumo0  1931  mo23  1941  mor  1942  modc  1943  eu2  1944  eu3h  1945  mo2r  1952  mo3h  1953  mo2dc  1955  mo4f  1960  eu4  1962  moim  1964  moimv  1966  moanim  1974  mopick  1978  2eu4  1993  euequ1  1995  exists1  1996  axext3  2023  axext4  2024  bm1.1  2025  cleqh  2137  cbvab  2160  sbab  2164  nfcjust  2166  drnfc1  2194  drnfc2  2195  dvelimdc  2197  dvelimc  2198  nfcvf  2199  cbvralf  2527  cbvrexf  2528  cbvreu  2531  cbvraldva2  2537  cbvrexdva2  2538  cbvraldva  2539  cbvrexdva  2540  cbvral2v  2541  cbvrex2v  2542  cbvral3v  2543  cbvrab  2555  vjust  2558  vex  2560  rr19.3v  2682  rr19.28v  2683  ralab2  2705  rexab2  2707  reu2  2729  reu6  2730  reu3  2731  rmo4  2734  reu4  2735  reu7  2736  reu8  2737  cdeqi  2749  cdeqri  2750  cdeqth  2751  cdeqnot  2752  cdeqal  2753  cdeqab  2754  cdeqim  2757  cdeqcv  2758  cdeqeq  2759  cdeqel  2760  nfccdeq  2762  sbsbc  2768  sbc8g  2771  sbcco2  2786  sbc5  2787  sbcralt  2834  sbcralg  2836  sbcreug  2838  rmo3  2849  cbvcsb  2856  sbcel12g  2865  sbceqg  2866  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  difjust  2919  unjust  2921  injust  2923  dfss2f  2936  dfnul3  3227  dfif3  3343  preq12bg  3544  eluniab  3592  elintab  3626  int0  3629  dfiunv2  3693  cbviun  3694  cbviin  3695  cbvdisj  3755  sndisj  3760  sbcbrg  3813  cbvmpt  3851  axsep2  3876  bm1.3ii  3878  nalset  3887  zfpow  3928  el  3931  dtruarb  3942  copsexg  3981  opelopabsb  3997  swopo  4043  pofun  4049  issod  4056  frind  4089  zfun  4171  ruv  4274  dtru  4284  tfisi  4310  findes  4326  relop  4486  dfdmf  4528  dfrnf  4575  resiexg  4653  dfres2  4658  opabresid  4659  mptresid  4660  imai  4681  issref  4707  intasym  4709  cnvi  4728  rnxpid  4755  cnvpom  4860  nfiota1  4869  cbviota  4872  sb8iota  4874  iotaval  4878  iotanul  4882  iota4  4885  csbiotag  4895  dffun2  4912  dffun4  4913  dffun5r  4914  dffun6f  4915  dffun4f  4918  sbcfung  4925  funcnveq  4962  fun11  4966  fununi  4967  funcnvuni  4968  imain  4981  isarep2  4986  brprcneu  5171  fv2  5173  elfv  5176  fv3  5197  relelfvdm  5205  fvmpt2  5254  ralrnmpt  5309  rexrnmpt  5310  ffnfvf  5324  f1veqaeq  5408  dff13f  5409  fliftfuns  5438  cbvriota  5478  csbriotag  5480  acexmid  5511  oprabidlem  5536  cbvmpt2x  5582  cbvmpt2  5583  cbvmpt2v  5584  mpt2fun  5603  abrexex2  5751  fmpt2co  5837  f1o2ndf1  5849  poxp  5853  tposoprab  5895  tfrlem3-2d  5928  tfrlemi1  5946  eqerlem  6137  qliftfuns  6190  eroveu  6197  idssen  6257  findcard2d  6348  nnwetri  6354  ordiso2  6357  ltsopi  6418  addpipqqs  6468  mulpipqqs  6471  archpr  6741  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemdisj  6749  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlemlim  6759  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdrl  6776  caucvgprprlemcbv  6785  caucvgprprlemopu  6797  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgsrlembound  6878  caucvgsrlembnd  6885  peano1nnnn  6928  axcaucvglemres  6973  1nn  7925  uzind4s  8533  uzind4s2  8534  indstr  8536  eqreznegel  8549  lbzbi  8551  qbtwnzlemstep  9103  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  iseqovex  9219  iseqcaopr3  9240  iseqdistr  9249  cvg1nlemres  9584  resqrexlemsqa  9622  resqrexlemex  9623  cau3lem  9710  fclim  9815  climeu  9817  cn1lem  9834  climcau  9866  climcvg1n  9869  spimd  9905  2spim  9906  ch2var  9907  bj-sbimedh  9911  bj-sbimeh  9912  cbvrald  9927  bdth  9951  bdcdeq  9959  bdne  9973  bdreu  9975  bdcsn  9990  bdsep2  10006  bdsepnft  10007  bdsepnfALT  10009  bdbm1.3ii  10011  bj-nalset  10015  bj-zfpair2  10030  bj-bdfindes  10074  bj-nn0suc0  10075  bj-nntrans  10076  setindft  10090  setindis  10092  bdsetindis  10094  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098  strcoll2  10108  strcollnft  10109  strcollnfALT  10111  sscoll2  10113
  Copyright terms: Public domain W3C validator