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

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

(Instead of introducing weq 1437 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 1289. This lets us avoid overloading the  = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1437 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1289. 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 1289 1  wff  x  =  y
Colors of variables: wff set class
Syntax hints:    = wceq 1289
This theorem is referenced by:  alequcoms  1454  equidqe  1470  ax4sp1  1471  equid  1634  nfequid  1635  stdpc6  1636  equcomi  1637  ax6evr  1638  equcom  1639  equcomd  1640  equcoms  1641  equtr  1642  equtrr  1643  equtr2  1644  equequ1  1645  equequ2  1646  elequ1  1647  elequ2  1648  ax11i  1649  ax10o  1650  ax10  1652  nfae  1654  hbaes  1655  hbnae  1656  nfnae  1657  hbnaes  1658  equsalh  1661  equsal  1662  dral1  1665  dral2  1666  drex2  1667  drnf1  1668  drnf2  1669  spimth  1670  spimh  1672  spimed  1675  cbv1  1679  cbv1h  1680  cbv2h  1681  cbvalh  1683  chvar  1687  sbimi  1694  sb1  1696  sb2  1697  sbequ1  1698  sbequ2  1699  sbequ12  1701  sbequ12r  1702  sbequ12a  1703  sbid  1704  stdpc4  1705  sbh  1706  sb6x  1709  sbequ5  1712  sbequ6  1713  equsb1  1715  equsb2  1716  sbiedh  1717  sbiedv  1719  sbieh  1720  equs5a  1722  drsb1  1727  exdistrfor  1728  sb4a  1729  equs45f  1730  sb6f  1731  sb5f  1732  sb4e  1733  hbsb2a  1734  hbsb2e  1735  sbcof2  1738  aev  1740  ax16  1741  dveeq2  1743  dveeq2or  1744  ax11v2  1748  ax11a2  1749  ax11b  1754  equs5  1757  equs5or  1758  sb3  1759  sb4  1760  sb4or  1761  sb4b  1762  sb4bor  1763  hbsb2  1764  nfsb2or  1765  sbequi  1767  sbequ  1768  drsb2  1769  spsbe  1770  spsbim  1771  sbequ8  1775  sbidm  1779  sb5rf  1780  sb6rf  1781  ax16i  1786  spv  1788  speiv  1790  equvin  1791  a16g  1792  a16gb  1793  a16nf  1794  sb56  1813  sb6  1814  sb5  1815  sbnv  1816  sbanv  1817  sborv  1818  sbi1v  1819  sbi2v  1820  cbval2  1844  cbvex2  1845  cbvaldva  1851  cbvexdva  1852  cbvex4v  1853  cleljust  1861  hbs1  1862  hbsbv  1865  nfsbxy  1866  nfsbxyt  1867  equsb3  1873  sbco  1890  sbcocom  1892  sbcomxyyz  1894  elsb3  1900  elsb4  1901  sb9v  1902  2sb5  1907  2sb6  1908  sbcom2v  1909  sb6a  1912  2sb5rf  1913  2sb6rf  1914  dfsb7  1915  sb7f  1916  sb7af  1917  sb10f  1919  sbel2x  1922  sbalyz  1923  sbal1yz  1925  sbal1  1926  sbexyz  1927  exsb  1932  2exsb  1933  dvelimALT  1934  dvelimfv  1935  hbsb4t  1937  nfsb4t  1938  dvelimf  1939  dvelimdf  1940  dvelimor  1942  dveeq1  1943  sbal2  1946  euf  1953  eubidh  1954  eubid  1955  hbeu1  1958  nfeu1  1959  sb8eu  1961  nfeuv  1966  sb8euh  1971  eu1  1973  mo2n  1976  euex  1978  eumo0  1979  mo23  1989  mor  1990  modc  1991  eu2  1992  eu3h  1993  mo2r  2000  mo3h  2001  mo2dc  2003  mo4f  2008  eu4  2010  moim  2012  moimv  2014  moanim  2022  mopick  2026  2eu4  2041  euequ1  2043  exists1  2044  axext3  2071  axext4  2072  bm1.1  2073  eleq1w  2148  cleqh  2187  cbvab  2210  sbab  2214  nfcjust  2216  drnfc1  2245  drnfc2  2246  dvelimdc  2248  dvelimc  2249  nfcvf  2250  cbvralf  2584  cbvrexf  2585  cbvreu  2588  cbvraldva2  2594  cbvrexdva2  2595  cbvraldva  2596  cbvrexdva  2597  cbvral2v  2598  cbvrex2v  2599  cbvral3v  2600  cbvrab  2617  vjust  2620  vex  2622  rr19.3v  2753  rr19.28v  2754  ralab2  2777  rexab2  2779  reu2  2801  reu6  2802  reu3  2803  rmo4  2806  reu4  2807  reu7  2808  reu8  2809  rmo3f  2810  rmo4f  2811  cdeqi  2823  cdeqri  2824  cdeqth  2825  cdeqnot  2826  cdeqal  2827  cdeqab  2828  cdeqim  2831  cdeqcv  2832  cdeqeq  2833  cdeqel  2834  nfccdeq  2836  sbsbc  2842  sbc8g  2845  sbcco2  2860  sbc5  2861  sbcralt  2913  sbcralg  2915  sbcreug  2917  rmo3  2928  cbvcsb  2935  sbcel12g  2944  sbceqg  2945  cbvralcsf  2988  cbvrexcsf  2989  cbvreucsf  2990  cbvrabcsf  2991  difjust  2998  unjust  3000  injust  3002  dfss2f  3014  dfdif3  3108  dfnul3  3287  dfif3  3402  preq12bg  3612  eluniab  3660  elintab  3694  int0  3697  dfiunv2  3761  cbviun  3762  cbviin  3763  cbvdisj  3824  disjiun  3832  sndisj  3833  sbcbrg  3886  cbvmptf  3924  cbvmpt  3925  axsep2  3950  bm1.3ii  3952  nalset  3961  zfpow  4002  el  4005  dtruarb  4017  copsexg  4062  opelopabsb  4078  swopo  4124  pofun  4130  issod  4137  frind  4170  zfun  4252  ruv  4356  dtru  4366  dcextest  4386  tfisi  4392  findes  4408  relop  4574  dfdmf  4617  dfrnf  4664  resiexg  4744  dfres2  4751  opabresid  4752  mptresid  4753  imai  4775  issref  4801  intasym  4803  cnvi  4823  rnxpid  4852  cnvpom  4960  nfiota1  4969  cbviota  4972  sb8iota  4974  iotaval  4978  iotanul  4982  iota4  4985  csbiotag  4995  dffun2  5012  dffun4  5013  dffun5r  5014  dffun6f  5015  dffun4f  5018  sbcfung  5025  funopg  5034  funinsn  5049  funcnveq  5063  fun11  5067  fununi  5068  funcnvuni  5069  imain  5082  isarep2  5087  brprcneu  5282  fv2  5284  elfv  5287  fv3  5312  relelfvdm  5320  fvmpt2  5370  ralrnmpt  5425  rexrnmpt  5426  ffnfvf  5441  f1veqaeq  5530  dff13f  5531  fliftfuns  5559  cbvriota  5600  csbriotag  5602  acexmid  5633  oprabidlem  5662  cbvmpt2x  5708  cbvmpt2  5709  cbvmpt2v  5710  mpt2fun  5729  abrexex2  5877  fmpt2co  5963  f1o2ndf1  5975  poxp  5979  tposoprab  6027  tfrlem3-2d  6059  tfrlemi1  6079  tfr1onlemsucfn  6087  tfr1onlemaccex  6095  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllembfn  6104  tfrcllemaccex  6108  dcdifsnid  6245  eqerlem  6303  qliftfuns  6356  eroveu  6363  idssen  6474  xpf1o  6540  xpmapen  6546  findcard2d  6587  nnwetri  6606  snexxph  6638  fidcenumlemim  6640  fidcenumlemrk  6642  fidcenum  6644  supmoti  6667  isoti  6681  supisoti  6684  cnvti  6693  ordiso2  6707  djuss  6740  ltsopi  6858  addpipqqs  6908  mulpipqqs  6911  archpr  7181  cauappcvgprlemlol  7185  cauappcvgprlemopu  7186  cauappcvgprlemupu  7187  cauappcvgprlemdisj  7189  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  cauappcvgprlemlim  7199  caucvgprlemlol  7208  caucvgprlemopu  7209  caucvgprlemupu  7210  caucvgprlemdisj  7212  caucvgprlemloc  7213  caucvgprlemcl  7214  caucvgprlemladdrl  7216  caucvgprprlemcbv  7225  caucvgprprlemopu  7237  caucvgprprlemclphr  7243  caucvgprprlemexbt  7244  caucvgsrlembound  7318  caucvgsrlembnd  7325  peano1nnnn  7368  axcaucvglemres  7413  negf1o  7839  lbreu  8378  lbinf  8381  suprubex  8384  suprlubex  8385  suprleubex  8387  1nn  8405  uzind4s  9047  uzind4s2  9048  indstr  9050  supinfneg  9052  infsupneg  9053  eqreznegel  9068  lbzbi  9070  exbtwnzlemex  9626  exbtwnz  9627  rebtwn2zlemstep  9629  rebtwn2z  9631  iseqovex  9835  iseqvalcbv  9837  seq3f1olemqsum  9894  seq3f1olemp  9896  seq3f1oleml  9897  iseqdistr  9910  seq3distr  9911  faclbnd6  10117  fimaxq  10200  cvg1nlemres  10383  resqrexlemsqa  10422  resqrexlemex  10423  cau3lem  10512  fclim  10646  climeu  10648  cn1lem  10666  climcau  10700  climcvg1n  10703  isummolem3  10734  isummolem2a  10735  isummolem2  10736  isummo  10737  zisum  10738  fisum  10742  isumz  10745  isumss2  10749  fisumsers  10751  fisumser  10753  fsumadd  10763  fsum2dlemstep  10791  fisumcom2  10795  isumshft  10846  cvgratz  10887  odd2np1lem  10965  zsupcl  11036  infssuzex  11038  infssuzledc  11039  bezoutlemmain  11080  bezoutlemeu  11089  gcdmultiple  11102  rplpwr  11109  pw2dvdseu  11239  hashdvds  11290  spimd  11323  2spim  11324  ch2var  11325  bj-sbimedh  11329  bj-sbimeh  11330  cbvrald  11345  sumdc2  11356  bdth  11379  bdcdeq  11387  bdne  11401  bdreu  11403  bdcsn  11418  bdsep2  11434  bdsepnft  11435  bdsepnfALT  11437  bdbm1.3ii  11439  bj-nalset  11443  bj-zfpair2  11458  bj-bdfindes  11501  bj-nn0suc0  11502  bj-nntrans  11503  setindft  11517  setindis  11519  bdsetindis  11521  bj-inf2vnlem3  11524  bj-inf2vnlem4  11525  strcoll2  11535  strcollnft  11536  strcollnfALT  11538  sscoll2  11540  nnti  11549  nnsf  11552  peano4nninf  11553  nninfsellemqall  11564  nninfomni  11568
  Copyright terms: Public domain W3C validator