NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  weq Unicode version

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

(Instead of introducing weq 1643 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 1642. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1643 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1642. 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

Proof of Theorem weq
StepHypRef Expression
1 wceq 1642 1
Colors of variables: wff setvar class
Syntax hints:   wceq 1642
This theorem is referenced by:  equs3  1644  speimfw  1645  spimfw  1646  ax11i  1647  sbequ2  1650  sb1  1651  sbimi  1652  a9ev  1656  exiftru  1657  exiftruOLD  1658  spimeh  1667  spimw  1668  spnfw  1670  equid  1676  equidOLD  1677  nfequid  1678  equcomi  1679  equcom  1680  equcoms  1681  equtr  1682  equtrr  1683  equequ1  1684  equequ1OLD  1685  equequ2  1686  stdpc6  1687  equtr2  1688  ax12b  1689  ax12bOLD  1690  spfw  1691  spnfwOLD  1692  spw  1694  spvwOLD  1695  spfalwOLD  1699  19.2OLD  1700  cbvalw  1701  cbvalvw  1702  cbvexvw  1703  alcomiw  1704  hba1w  1707  hbe1w  1708  elequ1  1713  elequ2  1715  ax9dgen  1716  ax11w  1721  ax11dgen  1722  ax11wdemo  1723  ax12w  1724  ax12dgen1  1725  ax12dgen2  1726  ax12dgen3  1727  sp  1747  spOLD  1748  spimehOLD  1821  equsalhw  1838  equsalhwOLD  1839  dvelimhw  1849  cbv3hv  1850  cbv3hvOLD  1851  equs5a  1887  equs5e  1888  sbequ1  1918  sbequ12  1919  sbequ12r  1920  sbequ12a  1921  sbid  1922  sb4a  1923  sb4e  1924  ax12olem1  1927  ax12olem2  1928  ax12olem3  1929  ax12olem4  1930  ax12olem5  1931  ax12olem6  1932  ax12  1935  ax10lem1  1936  ax10lem2  1937  ax10lem3  1938  dvelimv  1939  dveeq2  1940  ax10lem4  1941  ax10lem5  1942  ax10lem6  1943  ax10  1944  a16g  1945  aecoms  1947  naecoms  1948  ax9  1949  ax9o  1950  a9e  1951  ax10o  1952  hbae  1953  nfae  1954  hbnae  1955  nfnae  1956  hbnaes  1957  nfeqf  1958  equs4  1959  equsal  1960  equsex  1962  dvelimh  1964  dral1  1965  dral2  1966  drex1  1967  drex2  1968  drnf1  1969  drnf2  1970  exdistrf  1971  nfald2  1972  nfexd2  1973  spimt  1974  spim  1975  spime  1976  spimed  1977  cbv1h  1978  cbv2h  1980  cbv3  1982  cbv3h  1983  cbval  1984  cbvex  1985  chvar  1986  equvini  1987  equveli  1988  equs45f  1989  aev  1991  ax11v2  1992  ax11a2  1993  ax11b  1995  equs5  1996  dvelimf  1997  spv  1998  speiv  2000  equvin  2001  cbval2  2004  cbvex2  2005  cbvexd  2009  cbvaldva  2010  cbvexdva  2011  cbvex4v  2012  cleljust  2014  cleljustALT  2015  dveeq1  2018  ax15  2021  drsb1  2022  sb2  2023  stdpc4  2024  sbft  2025  sb6x  2029  sbequ5  2031  sbequ6  2032  equsb1  2034  equsb2  2035  sbied  2036  sbiedv  2037  sbie  2038  sb6f  2039  sb5f  2040  hbsb2a  2041  hbsb2e  2042  ax16i  2046  ax16ALT2  2048  a16gALT  2049  a16gb  2050  a16nf  2051  sb3  2052  sb4  2053  sb4b  2054  dfsb2  2055  dfsb3  2056  hbsb2  2057  nfsb2  2058  sbequi  2059  sbequ  2060  drsb2  2061  sbn  2062  sbi1  2063  sbequ8  2079  nfsb4t  2080  nfsb4  2081  dvelimdf  2082  sbco  2083  sbidm  2085  sbco2  2086  sbco3  2088  sbcom  2089  sb5rf  2090  sb6rf  2091  sb9i  2094  ax11v  2096  sb56  2098  sb6  2099  sb5  2100  equsb3lem  2101  equsb3  2102  hbs1  2105  nfsb  2109  nfsbd  2111  2sb5  2112  2sb6  2113  sbcom2  2114  pm11.07  2115  sb6a  2116  2sb5rf  2117  2sb6rf  2118  dfsb7  2119  sb7f  2120  sb10f  2122  sbelx  2124  sbel2x  2125  sbal1  2126  sbal  2127  exsb  2130  2exsb  2132  dvelimALT  2133  sbal2  2134  ax9from9o  2148  aecom-o  2151  aecoms-o  2152  hbae-o  2153  dral1-o  2154  ax11  2155  ax12from12o  2156  equid1  2158  hbequid  2160  nfequid-o  2161  equidqe  2173  ax4sp1  2174  equidq  2175  equid1ALT  2176  ax10from10o  2177  naecoms-o  2178  hbnae-o  2179  dvelimf-o  2180  dral2-o  2181  aev-o  2182  ax17eq  2183  dveeq2-o  2184  dveeq2-o16  2185  a16g-o  2186  dveeq1-o  2187  dveeq1-o16  2188  ax17el  2189  ax10-16  2190  ax11f  2192  ax11eq  2193  ax11el  2194  ax11indn  2195  ax11indi  2196  ax11indalem  2197  ax11inda2ALT  2198  ax11inda2  2199  ax11inda  2200  ax11v2-o  2201  ax11a2-o  2202  ax10o-o  2203  eujustALT  2207  eumo0  2228  eu2  2229  eu3  2230  mo2  2233  mo3  2235  mo4f  2236  eu4  2243  moanim  2260  2eu5  2288  euequ1  2292  axi11e  2332  cleqh  2450  nfrmod  2784  nfrmo  2786  cbvraldva2  2839  cbvrexdva2  2840  cbvraldva  2841  cbvrexdva  2842  cbvrex2v  2844  sbralie  2848  rmo4  3029  reu4  3030  2reu5lem3  3043  2reu5  3044  sbsbc  3050  sbc8g  3053  sbc2or  3054  sbcco2  3069  sbc5  3070  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  rmo2  3131  rmo2i  3132  rmo3  3133  sbcel12g  3151  sbceqg  3152  cbvralcsf  3198  cbvrabcsf  3201  ninjust  3210  csbifg  3690  axxpprim  4090  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  snex  4111  pwadjoin  4119  preqr2g  4126  preq12bg  4128  1cex  4142  opkabssvvk  4208  sikss1c1c  4267  opkelidkg  4274  idkssvvk  4281  dfpw12  4301  dfidk2  4313  unipw1  4325  eqpw1uni  4330  dfeu2  4333  sb8iota  4346  iota4  4357  csbiotag  4371  peano2  4403  addcid1  4405  nnc0suc  4412  nncaddccl  4419  nnsucelrlem1  4424  nnsucelr  4428  nndisjeq  4429  preaddccan2  4455  ltfintrilem1  4465  ltfintri  4466  ssfin  4470  vfinnc  4471  ncfinraise  4481  ncfinlower  4483  nnpw1ex  4484  eqtfinrelk  4486  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  evenodddisj  4516  nnadjoinlem1  4519  nnadjoin  4520  nnadjoinpw  4521  nnpweq  4523  sfindbl  4530  sfintfin  4532  tfinnn  4534  spfinsfincl  4539  vfinspsslem1  4550  vfinspss  4551  vfinspclt  4552  dfphi2  4569  phi11lem1  4595  proj1op  4600  proj2op  4601  copsexg  4607  phidisjnn  4615  phialllem1  4616  opeq  4619  cbvopab  4630  sbcbrg  4685  opelopabsb  4697  br1stg  4730  dfima2  4745  dfco1  4748  dfsi2  4751  opeliunxp  4820  ralxpf  4827  opabid2  4861  ideqg  4868  ideqg2  4869  dfdmf  4905  dmi  4919  iss  5000  dfres2  5002  opabresid  5003  intasym  5028  intirr  5029  dmsnopg  5066  coi1  5094  dfxp2  5113  dffun2  5119  dffun3  5120  dffun4  5121  dffun5  5122  dffun6f  5123  nfunv  5138  funun  5146  fun11  5159  fununi  5160  fun11iun  5305  fv2  5324  elfv  5326  tz6.12-2  5346  dffn5  5363  fnasrn  5417  fvi  5442  dff13  5471  isotr  5495  dfid4  5503  1stfo  5505  2ndfo  5506  swapf1o  5511  fununiq  5517  funsi  5520  oprabid  5550  cbvoprab12  5569  oprabid2  5646  mptresid  5720  trtxp  5781  brtxp  5783  elfix  5787  oqelins4  5794  fntxp  5804  addcfnex  5824  funsex  5828  qrpprod  5836  dmpprod  5840  fnpprod  5843  pw1fnf1o  5855  fnfullfunlem1  5856  fnfullfunlem2  5857  fvfullfunlem1  5861  fvfullfunlem2  5862  fvfullfunlem3  5863  clos1basesuc  5882  antisymex  5912  foundex  5914  extex  5915  frd  5922  extd  5923  antird  5928  antid  5929  frds  5935  weds  5938  po0  5939  ider  5943  ssetpov  5944  idssen  6040  fundmen  6043  xpassen  6057  enpw1lem1  6061  enpw1  6062  enmap2lem4  6066  enmap1lem4  6072  enprmaplem3  6078  enprmaplem5  6080  enprmaplem6  6081  nenpw1pwlem2  6085  mucex  6133  ncspw1eu  6159  ceex  6174  ce0addcnnul  6179  ce0nn  6180  el2c  6191  lecponc  6213  leconnnc  6218  dflec3  6221  tcfnex  6244  nclenn  6249  csucex  6259  nnltp1c  6262  addccan2nclem1  6263  addccan2nc  6265  nmembers1lem1  6268  nmembers1lem3  6270  nmembers1  6271  nncdiv3  6277  nnc3n3p1  6278  spacind  6287  nchoicelem3  6291  nchoicelem12  6300  nchoicelem17  6305  nchoicelem19  6307  fnfreclem1  6317  fnfrec  6320  scancan  6331
  Copyright terms: Public domain W3C validator