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

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

(Instead of introducing weq 1408 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 1259. This lets us avoid overloading the  = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1408 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1259. 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 1259 1  wff  x  =  y
Colors of variables: wff set class
Syntax hints:    = wceq 1259
This theorem is referenced by:  alequcoms  1425  equidqe  1441  ax4sp1  1442  equid  1605  nfequid  1606  stdpc6  1607  equcomi  1608  equcom  1609  equcoms  1610  equtr  1611  equtrr  1612  equtr2  1613  equequ1  1614  equequ2  1615  elequ1  1616  elequ2  1617  ax11i  1618  ax10o  1619  ax10  1621  nfae  1623  hbaes  1624  hbnae  1625  nfnae  1626  hbnaes  1627  equsalh  1630  equsal  1631  dral1  1634  dral2  1635  drex2  1636  drnf1  1637  drnf2  1638  spimth  1639  spimh  1641  spimed  1644  cbv1  1648  cbv1h  1649  cbv2h  1650  cbvalh  1652  chvar  1656  sbimi  1663  sb1  1665  sb2  1666  sbequ1  1667  sbequ2  1668  sbequ12  1670  sbequ12r  1671  sbequ12a  1672  sbid  1673  stdpc4  1674  sbh  1675  sb6x  1678  sbequ5  1681  sbequ6  1682  equsb1  1684  equsb2  1685  sbiedh  1686  sbiedv  1688  sbieh  1689  equs5a  1691  drsb1  1696  exdistrfor  1697  sb4a  1698  equs45f  1699  sb6f  1700  sb5f  1701  sb4e  1702  hbsb2a  1703  hbsb2e  1704  sbcof2  1707  aev  1709  ax16  1710  dveeq2  1712  dveeq2or  1713  ax11v2  1717  ax11a2  1718  ax11b  1723  equs5  1726  equs5or  1727  sb3  1728  sb4  1729  sb4or  1730  sb4b  1731  sb4bor  1732  hbsb2  1733  nfsb2or  1734  sbequi  1736  sbequ  1737  drsb2  1738  spsbe  1739  spsbim  1740  sbequ8  1743  sbidm  1747  sb5rf  1748  sb6rf  1749  ax16i  1754  spv  1756  speiv  1758  equvin  1759  a16g  1760  a16gb  1761  a16nf  1762  sb56  1781  sb6  1782  sb5  1783  sbnv  1784  sbanv  1785  sborv  1786  sbi1v  1787  sbi2v  1788  cbval2  1812  cbvex2  1813  cbvaldva  1819  cbvexdva  1820  cbvex4v  1821  cleljust  1829  hbs1  1830  hbsbv  1833  nfsbxy  1834  nfsbxyt  1835  equsb3  1841  sbco  1858  sbcocom  1860  sbcomxyyz  1862  elsb3  1868  elsb4  1869  sb9v  1870  2sb5  1875  2sb6  1876  sbcom2v  1877  sb6a  1880  2sb5rf  1881  2sb6rf  1882  dfsb7  1883  sb7f  1884  sb7af  1885  sb10f  1887  sbel2x  1890  sbalyz  1891  sbal1yz  1893  sbal1  1894  sbexyz  1895  exsb  1900  2exsb  1901  dvelimALT  1902  dvelimfv  1903  hbsb4t  1905  nfsb4t  1906  dvelimf  1907  dvelimdf  1908  dvelimor  1910  dveeq1  1911  sbal2  1914  euf  1921  eubidh  1922  eubid  1923  hbeu1  1926  nfeu1  1927  sb8eu  1929  nfeuv  1934  sb8euh  1939  eu1  1941  mo2n  1944  euex  1946  eumo0  1947  mo23  1957  mor  1958  modc  1959  eu2  1960  eu3h  1961  mo2r  1968  mo3h  1969  mo2dc  1971  mo4f  1976  eu4  1978  moim  1980  moimv  1982  moanim  1990  mopick  1994  2eu4  2009  euequ1  2011  exists1  2012  axext3  2039  axext4  2040  bm1.1  2041  cleqh  2153  cbvab  2176  sbab  2180  nfcjust  2182  drnfc1  2210  drnfc2  2211  dvelimdc  2213  dvelimc  2214  nfcvf  2215  cbvralf  2544  cbvrexf  2545  cbvreu  2548  cbvraldva2  2554  cbvrexdva2  2555  cbvraldva  2556  cbvrexdva  2557  cbvral2v  2558  cbvrex2v  2559  cbvral3v  2560  cbvrab  2572  vjust  2575  vex  2577  rr19.3v  2705  rr19.28v  2706  ralab2  2728  rexab2  2730  reu2  2752  reu6  2753  reu3  2754  rmo4  2757  reu4  2758  reu7  2759  reu8  2760  cdeqi  2772  cdeqri  2773  cdeqth  2774  cdeqnot  2775  cdeqal  2776  cdeqab  2777  cdeqim  2780  cdeqcv  2781  cdeqeq  2782  cdeqel  2783  nfccdeq  2785  sbsbc  2791  sbc8g  2794  sbcco2  2809  sbc5  2810  sbcralt  2862  sbcralg  2864  sbcreug  2866  rmo3  2877  cbvcsb  2884  sbcel12g  2893  sbceqg  2894  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  difjust  2947  unjust  2949  injust  2951  dfss2f  2964  dfnul3  3255  dfif3  3371  preq12bg  3572  eluniab  3620  elintab  3654  int0  3657  dfiunv2  3721  cbviun  3722  cbviin  3723  cbvdisj  3783  sndisj  3788  sbcbrg  3841  cbvmpt  3879  axsep2  3904  bm1.3ii  3906  nalset  3915  zfpow  3956  el  3959  dtruarb  3970  copsexg  4009  opelopabsb  4025  swopo  4071  pofun  4077  issod  4084  frind  4117  zfun  4199  ruv  4302  dtru  4312  tfisi  4338  findes  4354  relop  4514  dfdmf  4556  dfrnf  4603  resiexg  4681  dfres2  4686  opabresid  4687  mptresid  4688  imai  4709  issref  4735  intasym  4737  cnvi  4756  rnxpid  4783  cnvpom  4888  nfiota1  4897  cbviota  4900  sb8iota  4902  iotaval  4906  iotanul  4910  iota4  4913  csbiotag  4923  dffun2  4940  dffun4  4941  dffun5r  4942  dffun6f  4943  dffun4f  4946  sbcfung  4953  funcnveq  4990  fun11  4994  fununi  4995  funcnvuni  4996  imain  5009  isarep2  5014  brprcneu  5199  fv2  5201  elfv  5204  fv3  5225  relelfvdm  5233  fvmpt2  5282  ralrnmpt  5337  rexrnmpt  5338  ffnfvf  5352  f1veqaeq  5436  dff13f  5437  fliftfuns  5466  cbvriota  5506  csbriotag  5508  acexmid  5539  oprabidlem  5564  cbvmpt2x  5610  cbvmpt2  5611  cbvmpt2v  5612  mpt2fun  5631  abrexex2  5779  fmpt2co  5865  f1o2ndf1  5877  poxp  5881  tposoprab  5926  tfrlem3-2d  5959  tfrlemi1  5977  eqerlem  6168  qliftfuns  6221  eroveu  6228  idssen  6288  findcard2d  6379  nnwetri  6385  supmoti  6399  isoti  6411  supisoti  6414  ordiso2  6415  ltsopi  6476  addpipqqs  6526  mulpipqqs  6529  archpr  6799  cauappcvgprlemlol  6803  cauappcvgprlemopu  6804  cauappcvgprlemupu  6805  cauappcvgprlemdisj  6807  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlemlim  6817  caucvgprlemlol  6826  caucvgprlemopu  6827  caucvgprlemupu  6828  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemcl  6832  caucvgprlemladdrl  6834  caucvgprprlemcbv  6843  caucvgprprlemopu  6855  caucvgprprlemclphr  6861  caucvgprprlemexbt  6862  caucvgsrlembound  6936  caucvgsrlembnd  6943  peano1nnnn  6986  axcaucvglemres  7031  1nn  8001  uzind4s  8629  uzind4s2  8630  indstr  8632  eqreznegel  8646  lbzbi  8648  qbtwnzlemstep  9205  qbtwnzlemex  9207  qbtwnz  9208  rebtwn2zlemstep  9209  rebtwn2z  9211  iseqovex  9383  iseqcaopr3  9404  iseqdistr  9414  faclbnd6  9612  cvg1nlemres  9812  resqrexlemsqa  9851  resqrexlemex  9852  cau3lem  9941  fclim  10046  climeu  10048  cn1lem  10065  climcau  10097  climcvg1n  10100  odd2np1lem  10183  pw2dvdseu  10256  spimd  10292  2spim  10293  ch2var  10294  bj-sbimedh  10298  bj-sbimeh  10299  cbvrald  10314  bdth  10338  bdcdeq  10346  bdne  10360  bdreu  10362  bdcsn  10377  bdsep2  10393  bdsepnft  10394  bdsepnfALT  10396  bdbm1.3ii  10398  bj-nalset  10402  bj-zfpair2  10417  bj-bdfindes  10461  bj-nn0suc0  10462  bj-nntrans  10463  setindft  10477  setindis  10479  bdsetindis  10481  bj-inf2vnlem3  10484  bj-inf2vnlem4  10485  strcoll2  10495  strcollnft  10496  strcollnfALT  10498  sscoll2  10500
  Copyright terms: Public domain W3C validator