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

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

(Instead of introducing weq 1389 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 1242. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1389 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1242. 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 1242 1 wff x = y
Colors of variables: wff set class
Syntax hints:   = wceq 1242
This theorem is referenced by:  alequcoms  1406  equidqe  1422  ax4sp1  1423  equid  1586  nfequid  1587  stdpc6  1588  equcomi  1589  equcom  1590  equcoms  1591  equtr  1592  equtrr  1593  equtr2  1594  equequ1  1595  equequ2  1596  elequ1  1597  elequ2  1598  ax11i  1599  ax10o  1600  ax10  1602  nfae  1604  hbaes  1605  hbnae  1606  nfnae  1607  hbnaes  1608  equsalh  1611  equsal  1612  dral1  1615  dral2  1616  drex2  1617  drnf1  1618  drnf2  1619  spimth  1620  spimh  1622  spimed  1625  cbv1  1629  cbv1h  1630  cbv2h  1631  cbvalh  1633  chvar  1637  sbimi  1644  sb1  1646  sb2  1647  sbequ1  1648  sbequ2  1649  sbequ12  1651  sbequ12r  1652  sbequ12a  1653  sbid  1654  stdpc4  1655  sbh  1656  sb6x  1659  sbequ5  1662  sbequ6  1663  equsb1  1665  equsb2  1666  sbiedh  1667  sbiedv  1669  sbieh  1670  equs5a  1672  drsb1  1677  exdistrfor  1678  sb4a  1679  equs45f  1680  sb6f  1681  sb5f  1682  sb4e  1683  hbsb2a  1684  hbsb2e  1685  sbcof2  1688  aev  1690  ax16  1691  dveeq2  1693  dveeq2or  1694  ax11v2  1698  ax11a2  1699  ax11b  1704  equs5  1707  equs5or  1708  sb3  1709  sb4  1710  sb4or  1711  sb4b  1712  sb4bor  1713  hbsb2  1714  nfsb2or  1715  sbequi  1717  sbequ  1718  drsb2  1719  spsbe  1720  spsbim  1721  sbequ8  1724  sbidm  1728  sb5rf  1729  sb6rf  1730  ax16i  1735  spv  1737  speiv  1739  equvin  1740  a16g  1741  a16gb  1742  a16nf  1743  sb56  1762  sb6  1763  sb5  1764  sbnv  1765  sbanv  1766  sborv  1767  sbi1v  1768  sbi2v  1769  cbval2  1793  cbvex2  1794  cbvaldva  1800  cbvexdva  1801  cbvex4v  1802  cleljust  1810  hbs1  1811  hbsbv  1814  nfsbxy  1815  nfsbxyt  1816  equsb3  1822  sbco  1839  sbcocom  1841  sbcomxyyz  1843  elsb3  1849  elsb4  1850  sb9v  1851  2sb5  1856  2sb6  1857  sbcom2v  1858  sb6a  1861  2sb5rf  1862  2sb6rf  1863  dfsb7  1864  sb7f  1865  sb7af  1866  sb10f  1868  sbel2x  1871  sbalyz  1872  sbal1yz  1874  sbal1  1875  sbexyz  1876  exsb  1881  2exsb  1882  dvelimALT  1883  dvelimfv  1884  hbsb4t  1886  nfsb4t  1887  dvelimf  1888  dvelimdf  1889  dvelimor  1891  dveeq1  1892  sbal2  1895  euf  1902  eubidh  1903  eubid  1904  hbeu1  1907  nfeu1  1908  sb8eu  1910  nfeuv  1915  sb8euh  1920  eu1  1922  mo2n  1925  euex  1927  eumo0  1928  mo23  1938  mor  1939  modc  1940  eu2  1941  eu3h  1942  mo2r  1949  mo3h  1950  mo2dc  1952  mo4f  1957  eu4  1959  moim  1961  moimv  1963  moanim  1971  mopick  1975  2eu4  1990  euequ1  1992  exists1  1993  axext3  2020  axext4  2021  bm1.1  2022  cleqh  2134  cbvab  2157  sbab  2161  nfcjust  2163  drnfc1  2191  drnfc2  2192  dvelimdc  2194  dvelimc  2195  nfcvf  2196  cbvralf  2521  cbvrexf  2522  cbvreu  2525  cbvraldva2  2531  cbvrexdva2  2532  cbvraldva  2533  cbvrexdva  2534  cbvral2v  2535  cbvrex2v  2536  cbvral3v  2537  cbvrab  2549  vjust  2552  vex  2554  rr19.3v  2676  rr19.28v  2677  ralab2  2699  rexab2  2701  reu2  2723  reu6  2724  reu3  2725  rmo4  2728  reu4  2729  reu7  2730  reu8  2731  cdeqi  2743  cdeqri  2744  cdeqth  2745  cdeqnot  2746  cdeqal  2747  cdeqab  2748  cdeqim  2751  cdeqcv  2752  cdeqeq  2753  cdeqel  2754  nfccdeq  2756  sbsbc  2762  sbc8g  2765  sbcco2  2780  sbc5  2781  sbcralt  2828  sbcralg  2830  sbcrexg  2831  sbcreug  2832  rmo3  2843  cbvcsb  2850  sbcel12g  2859  sbceqg  2860  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  difjust  2913  unjust  2915  injust  2917  dfss2f  2930  dfnul3  3221  dfif3  3337  preq12bg  3535  eluniab  3583  elintab  3617  int0  3620  dfiunv2  3684  cbviun  3685  cbviin  3686  cbvdisj  3746  sndisj  3751  sbcbrg  3804  cbvmpt  3842  axsep2  3867  bm1.3ii  3869  nalset  3878  zfpow  3919  el  3922  dtruarb  3933  copsexg  3972  opelopabsb  3988  swopo  4034  pofun  4040  issod  4047  zfun  4137  ruv  4228  dtru  4238  tfisi  4253  findes  4269  relop  4429  dfdmf  4471  dfrnf  4518  resiexg  4596  dfres2  4601  opabresid  4602  mptresid  4603  imai  4624  issref  4650  intasym  4652  cnvi  4671  rnxpid  4698  cnvpom  4803  nfiota1  4812  cbviota  4815  sb8iota  4817  iotaval  4821  iotanul  4825  iota4  4828  csbiotag  4838  dffun2  4855  dffun4  4856  dffun5r  4857  dffun6f  4858  dffun4f  4861  sbcfung  4868  funcnveq  4905  fun11  4909  fununi  4910  funcnvuni  4911  imain  4924  isarep2  4929  brprcneu  5114  fv2  5116  elfv  5119  fv3  5140  relelfvdm  5148  fvmpt2  5197  ralrnmpt  5252  rexrnmpt  5253  ffnfvf  5267  f1veqaeq  5351  dff13f  5352  fliftfuns  5381  cbvriota  5421  csbriotag  5423  acexmid  5454  oprabidlem  5479  cbvmpt2x  5524  cbvmpt2  5525  cbvmpt2v  5526  mpt2fun  5545  abrexex2  5693  fmpt2co  5779  f1o2ndf1  5791  poxp  5794  tposoprab  5836  tfrlem3-2d  5869  tfrlemi1  5887  eqerlem  6073  qliftfuns  6126  eroveu  6133  idssen  6193  ltsopi  6304  addpipqqs  6354  mulpipqqs  6357  archpr  6615  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemupu  6621  cauappcvgprlemdisj  6623  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlemlim  6633  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemupu  6643  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdrl  6649  1nn  7706  uzind4s  8309  uzind4s2  8310  indstr  8312  eqreznegel  8325  lbzbi  8327  iseqovex  8899  spimd  9240  2spim  9241  ch2var  9242  bj-sbimedh  9246  bj-sbimeh  9247  cbvrald  9262  bdth  9286  bdcdeq  9294  bdne  9308  bdreu  9310  bdcsn  9325  bdsep2  9341  bdsepnft  9342  bdsepnfALT  9344  bdbm1.3ii  9346  bj-nalset  9350  bj-zfpair2  9365  bj-bdfindes  9409  bj-nn0suc0  9410  bj-nntrans  9411  setindft  9425  setindis  9427  bdsetindis  9429  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433  strcoll2  9443  strcollnft  9444  strcollnfALT  9446  sscoll2  9448
  Copyright terms: Public domain W3C validator