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

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

(Instead of introducing weq 1433 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 1285. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1433 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1285. 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 1285 1 wff 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:   = wceq 1285
This theorem is referenced by:  alequcoms  1450  equidqe  1466  ax4sp1  1467  equid  1630  nfequid  1631  stdpc6  1632  equcomi  1633  ax6evr  1634  equcom  1635  equcoms  1636  equtr  1637  equtrr  1638  equtr2  1639  equequ1  1640  equequ2  1641  elequ1  1642  elequ2  1643  ax11i  1644  ax10o  1645  ax10  1647  nfae  1649  hbaes  1650  hbnae  1651  nfnae  1652  hbnaes  1653  equsalh  1656  equsal  1657  dral1  1660  dral2  1661  drex2  1662  drnf1  1663  drnf2  1664  spimth  1665  spimh  1667  spimed  1670  cbv1  1674  cbv1h  1675  cbv2h  1676  cbvalh  1678  chvar  1682  sbimi  1689  sb1  1691  sb2  1692  sbequ1  1693  sbequ2  1694  sbequ12  1696  sbequ12r  1697  sbequ12a  1698  sbid  1699  stdpc4  1700  sbh  1701  sb6x  1704  sbequ5  1707  sbequ6  1708  equsb1  1710  equsb2  1711  sbiedh  1712  sbiedv  1714  sbieh  1715  equs5a  1717  drsb1  1722  exdistrfor  1723  sb4a  1724  equs45f  1725  sb6f  1726  sb5f  1727  sb4e  1728  hbsb2a  1729  hbsb2e  1730  sbcof2  1733  aev  1735  ax16  1736  dveeq2  1738  dveeq2or  1739  ax11v2  1743  ax11a2  1744  ax11b  1749  equs5  1752  equs5or  1753  sb3  1754  sb4  1755  sb4or  1756  sb4b  1757  sb4bor  1758  hbsb2  1759  nfsb2or  1760  sbequi  1762  sbequ  1763  drsb2  1764  spsbe  1765  spsbim  1766  sbequ8  1770  sbidm  1774  sb5rf  1775  sb6rf  1776  ax16i  1781  spv  1783  speiv  1785  equvin  1786  a16g  1787  a16gb  1788  a16nf  1789  sb56  1808  sb6  1809  sb5  1810  sbnv  1811  sbanv  1812  sborv  1813  sbi1v  1814  sbi2v  1815  cbval2  1839  cbvex2  1840  cbvaldva  1846  cbvexdva  1847  cbvex4v  1848  cleljust  1856  hbs1  1857  hbsbv  1860  nfsbxy  1861  nfsbxyt  1862  equsb3  1868  sbco  1885  sbcocom  1887  sbcomxyyz  1889  elsb3  1895  elsb4  1896  sb9v  1897  2sb5  1902  2sb6  1903  sbcom2v  1904  sb6a  1907  2sb5rf  1908  2sb6rf  1909  dfsb7  1910  sb7f  1911  sb7af  1912  sb10f  1914  sbel2x  1917  sbalyz  1918  sbal1yz  1920  sbal1  1921  sbexyz  1922  exsb  1927  2exsb  1928  dvelimALT  1929  dvelimfv  1930  hbsb4t  1932  nfsb4t  1933  dvelimf  1934  dvelimdf  1935  dvelimor  1937  dveeq1  1938  sbal2  1941  euf  1948  eubidh  1949  eubid  1950  hbeu1  1953  nfeu1  1954  sb8eu  1956  nfeuv  1961  sb8euh  1966  eu1  1968  mo2n  1971  euex  1973  eumo0  1974  mo23  1984  mor  1985  modc  1986  eu2  1987  eu3h  1988  mo2r  1995  mo3h  1996  mo2dc  1998  mo4f  2003  eu4  2005  moim  2007  moimv  2009  moanim  2017  mopick  2021  2eu4  2036  euequ1  2038  exists1  2039  axext3  2066  axext4  2067  bm1.1  2068  eleq1w  2143  cleqh  2182  cbvab  2205  sbab  2209  nfcjust  2211  drnfc1  2239  drnfc2  2240  dvelimdc  2242  dvelimc  2243  nfcvf  2244  cbvralf  2577  cbvrexf  2578  cbvreu  2581  cbvraldva2  2587  cbvrexdva2  2588  cbvraldva  2589  cbvrexdva  2590  cbvral2v  2591  cbvrex2v  2592  cbvral3v  2593  cbvrab  2609  vjust  2612  vex  2614  rr19.3v  2742  rr19.28v  2743  ralab2  2766  rexab2  2768  reu2  2790  reu6  2791  reu3  2792  rmo4  2795  reu4  2796  reu7  2797  reu8  2798  cdeqi  2810  cdeqri  2811  cdeqth  2812  cdeqnot  2813  cdeqal  2814  cdeqab  2815  cdeqim  2818  cdeqcv  2819  cdeqeq  2820  cdeqel  2821  nfccdeq  2823  sbsbc  2829  sbc8g  2832  sbcco2  2847  sbc5  2848  sbcralt  2900  sbcralg  2902  sbcreug  2904  rmo3  2915  cbvcsb  2922  sbcel12g  2931  sbceqg  2932  cbvralcsf  2974  cbvrexcsf  2975  cbvreucsf  2976  cbvrabcsf  2977  difjust  2984  unjust  2986  injust  2988  dfss2f  3000  dfdif3  3093  dfnul3  3271  dfif3  3382  preq12bg  3586  eluniab  3634  elintab  3668  int0  3671  dfiunv2  3735  cbviun  3736  cbviin  3737  cbvdisj  3797  sndisj  3802  sbcbrg  3855  cbvmpt  3893  axsep2  3918  bm1.3ii  3920  nalset  3929  zfpow  3970  el  3973  dtruarb  3983  copsexg  4028  opelopabsb  4044  swopo  4090  pofun  4096  issod  4103  frind  4136  zfun  4218  ruv  4322  dtru  4332  tfisi  4357  findes  4373  relop  4535  dfdmf  4577  dfrnf  4624  resiexg  4704  dfres2  4709  opabresid  4710  mptresid  4711  imai  4732  issref  4758  intasym  4760  cnvi  4779  rnxpid  4806  cnvpom  4911  nfiota1  4920  cbviota  4923  sb8iota  4925  iotaval  4929  iotanul  4933  iota4  4936  csbiotag  4946  dffun2  4963  dffun4  4964  dffun5r  4965  dffun6f  4966  dffun4f  4969  sbcfung  4976  funopg  4985  funinsn  5000  funcnveq  5014  fun11  5018  fununi  5019  funcnvuni  5020  imain  5033  isarep2  5038  brprcneu  5224  fv2  5226  elfv  5229  fv3  5251  relelfvdm  5259  fvmpt2  5308  ralrnmpt  5363  rexrnmpt  5364  ffnfvf  5378  f1veqaeq  5462  dff13f  5463  fliftfuns  5491  cbvriota  5531  csbriotag  5533  acexmid  5564  oprabidlem  5589  cbvmpt2x  5635  cbvmpt2  5636  cbvmpt2v  5637  mpt2fun  5656  abrexex2  5804  fmpt2co  5890  f1o2ndf1  5902  poxp  5906  tposoprab  5951  tfrlem3-2d  5983  tfrlemi1  6003  tfr1onlemsucfn  6011  tfr1onlemaccex  6019  tfrcllemsucfn  6024  tfrcllemsucaccv  6025  tfrcllembxssdm  6027  tfrcllembfn  6028  tfrcllemaccex  6032  dcdifsnid  6168  eqerlem  6226  qliftfuns  6279  eroveu  6286  idssen  6347  xpf1o  6408  findcard2d  6449  nnwetri  6462  supmoti  6502  isoti  6516  supisoti  6519  cnvti  6528  ordiso2  6542  djuss  6565  ltsopi  6649  addpipqqs  6699  mulpipqqs  6702  archpr  6972  cauappcvgprlemlol  6976  cauappcvgprlemopu  6977  cauappcvgprlemupu  6978  cauappcvgprlemdisj  6980  cauappcvgprlemladdru  6985  cauappcvgprlemladdrl  6986  cauappcvgprlemlim  6990  caucvgprlemlol  6999  caucvgprlemopu  7000  caucvgprlemupu  7001  caucvgprlemdisj  7003  caucvgprlemloc  7004  caucvgprlemcl  7005  caucvgprlemladdrl  7007  caucvgprprlemcbv  7016  caucvgprprlemopu  7028  caucvgprprlemclphr  7034  caucvgprprlemexbt  7035  caucvgsrlembound  7109  caucvgsrlembnd  7116  peano1nnnn  7159  axcaucvglemres  7204  negf1o  7630  lbreu  8167  lbinf  8170  suprubex  8173  suprlubex  8174  suprleubex  8176  1nn  8194  uzind4s  8836  uzind4s2  8837  indstr  8839  supinfneg  8841  infsupneg  8842  eqreznegel  8857  lbzbi  8859  exbtwnzlemex  9413  exbtwnz  9414  rebtwn2zlemstep  9416  rebtwn2z  9418  iseqovex  9606  iseqvalcbv  9608  iseqdistr  9644  faclbnd6  9845  cvg1nlemres  10097  resqrexlemsqa  10136  resqrexlemex  10137  cau3lem  10226  fclim  10359  climeu  10361  cn1lem  10378  climcau  10410  climcvg1n  10413  odd2np1lem  10504  zsupcl  10575  infssuzex  10577  infssuzledc  10578  bezoutlemmain  10619  bezoutlemeu  10628  gcdmultiple  10641  rplpwr  10648  pw2dvdseu  10778  hashdvds  10829  spimd  10861  2spim  10862  ch2var  10863  bj-sbimedh  10867  bj-sbimeh  10868  cbvrald  10883  sumdc2  10894  bdth  10914  bdcdeq  10922  bdne  10936  bdreu  10938  bdcsn  10953  bdsep2  10969  bdsepnft  10970  bdsepnfALT  10972  bdbm1.3ii  10974  bj-nalset  10978  bj-zfpair2  10993  bj-bdfindes  11036  bj-nn0suc0  11037  bj-nntrans  11038  setindft  11052  setindis  11054  bdsetindis  11056  bj-inf2vnlem3  11059  bj-inf2vnlem4  11060  strcoll2  11070  strcollnft  11071  strcollnfALT  11073  sscoll2  11075
  Copyright terms: Public domain W3C validator