ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  weq GIF 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 𝑥 = 𝑦

Proof of Theorem weq
StepHypRef Expression
1 wceq 1259 1 wff 𝑥 = 𝑦
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  2704  rr19.28v  2705  ralab2  2727  rexab2  2729  reu2  2751  reu6  2752  reu3  2753  rmo4  2756  reu4  2757  reu7  2758  reu8  2759  cdeqi  2771  cdeqri  2772  cdeqth  2773  cdeqnot  2774  cdeqal  2775  cdeqab  2776  cdeqim  2779  cdeqcv  2780  cdeqeq  2781  cdeqel  2782  nfccdeq  2784  sbsbc  2790  sbc8g  2793  sbcco2  2808  sbc5  2809  sbcralt  2861  sbcralg  2863  sbcreug  2865  rmo3  2876  cbvcsb  2883  sbcel12g  2892  sbceqg  2893  cbvralcsf  2935  cbvrexcsf  2936  cbvreucsf  2937  cbvrabcsf  2938  difjust  2946  unjust  2948  injust  2950  dfss2f  2963  dfnul3  3254  dfif3  3370  preq12bg  3571  eluniab  3619  elintab  3653  int0  3656  dfiunv2  3720  cbviun  3721  cbviin  3722  cbvdisj  3782  sndisj  3787  sbcbrg  3840  cbvmpt  3878  axsep2  3903  bm1.3ii  3905  nalset  3914  zfpow  3955  el  3958  dtruarb  3969  copsexg  4008  opelopabsb  4024  swopo  4070  pofun  4076  issod  4083  frind  4116  zfun  4198  ruv  4301  dtru  4311  tfisi  4337  findes  4353  relop  4513  dfdmf  4555  dfrnf  4602  resiexg  4680  dfres2  4685  opabresid  4686  mptresid  4687  imai  4708  issref  4734  intasym  4736  cnvi  4755  rnxpid  4782  cnvpom  4887  nfiota1  4896  cbviota  4899  sb8iota  4901  iotaval  4905  iotanul  4909  iota4  4912  csbiotag  4922  dffun2  4939  dffun4  4940  dffun5r  4941  dffun6f  4942  dffun4f  4945  sbcfung  4952  funcnveq  4989  fun11  4993  fununi  4994  funcnvuni  4995  imain  5008  isarep2  5013  brprcneu  5198  fv2  5200  elfv  5203  fv3  5224  relelfvdm  5232  fvmpt2  5281  ralrnmpt  5336  rexrnmpt  5337  ffnfvf  5351  f1veqaeq  5435  dff13f  5436  fliftfuns  5465  cbvriota  5505  csbriotag  5507  acexmid  5538  oprabidlem  5563  cbvmpt2x  5609  cbvmpt2  5610  cbvmpt2v  5611  mpt2fun  5630  abrexex2  5778  fmpt2co  5864  f1o2ndf1  5876  poxp  5880  tposoprab  5925  tfrlem3-2d  5958  tfrlemi1  5976  eqerlem  6167  qliftfuns  6220  eroveu  6227  idssen  6287  findcard2d  6378  nnwetri  6384  supmoti  6398  isoti  6410  supisoti  6413  ordiso2  6414  ltsopi  6475  addpipqqs  6525  mulpipqqs  6528  archpr  6798  cauappcvgprlemlol  6802  cauappcvgprlemopu  6803  cauappcvgprlemupu  6804  cauappcvgprlemdisj  6806  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  cauappcvgprlemlim  6816  caucvgprlemlol  6825  caucvgprlemopu  6826  caucvgprlemupu  6827  caucvgprlemdisj  6829  caucvgprlemloc  6830  caucvgprlemcl  6831  caucvgprlemladdrl  6833  caucvgprprlemcbv  6842  caucvgprprlemopu  6854  caucvgprprlemclphr  6860  caucvgprprlemexbt  6861  caucvgsrlembound  6935  caucvgsrlembnd  6942  peano1nnnn  6985  axcaucvglemres  7030  1nn  8000  uzind4s  8628  uzind4s2  8629  indstr  8631  eqreznegel  8645  lbzbi  8647  qbtwnzlemstep  9204  qbtwnzlemex  9206  qbtwnz  9207  rebtwn2zlemstep  9208  rebtwn2z  9210  iseqovex  9382  iseqcaopr3  9403  iseqdistr  9413  faclbnd6  9611  cvg1nlemres  9811  resqrexlemsqa  9850  resqrexlemex  9851  cau3lem  9940  fclim  10045  climeu  10047  cn1lem  10064  climcau  10096  climcvg1n  10099  odd2np1lem  10182  pw2dvdseu  10235  spimd  10271  2spim  10272  ch2var  10273  bj-sbimedh  10277  bj-sbimeh  10278  cbvrald  10293  bdth  10317  bdcdeq  10325  bdne  10339  bdreu  10341  bdcsn  10356  bdsep2  10372  bdsepnft  10373  bdsepnfALT  10375  bdbm1.3ii  10377  bj-nalset  10381  bj-zfpair2  10396  bj-bdfindes  10440  bj-nn0suc0  10441  bj-nntrans  10442  setindft  10456  setindis  10458  bdsetindis  10460  bj-inf2vnlem3  10463  bj-inf2vnlem4  10464  strcoll2  10474  strcollnft  10475  strcollnfALT  10477  sscoll2  10479
  Copyright terms: Public domain W3C validator