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 set 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  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  iota4  4357  csbiotag  4371  peano2  4403  addcid1  4405  nnc0suc  4411  nncaddccl  4418  nnsucelrlem1  4423  nnsucelr  4427  nndisjeq  4428  preaddccan1lem1  4453  preaddccan1  4454  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  4593  proj1op  4598  proj2op  4599  copsexg  4605  phidisjnn  4613  cbvopab  4622  sbcbrg  4677  opelopabsb  4689  br1stg  4722  dfima2  4737  dfco1  4740  dfsi2  4743  ralxpf  4813  ideqg  4880  ideqg2  4881  dfdmf  4917  dmi  4931  iss  5015  dfres2  5017  opabresid  5018  intasym  5045  intirr  5046  dmsnopg  5086  coi1  5123  dfxp2  5146  dffun2  5152  nfunv  5172  funun  5180  fun11iun  5345  fv2  5364  elfv  5366  tz6.12-2  5386  dffn5  5403  fnasrn  5457  fvi  5482  dff13  5511  isotr  5535  dfid4  5544  1stfo  5546  2ndfo  5547  swapf1o  5552  fununiq  5558  funsi  5562  oprabid  5589  cbvoprab12  5609  mptresid  5760  trtxp  5809  brtxp  5811  elfix  5816  oqelins4  5823  fntxp  5834  addcfnex  5852  funsex  5856  qrpprod  5860  dmpprod  5866  fnpprod  5869  pw1fnf1o  5881  fnfullfunlem1  5882  fnfullfunlem2  5883  fvfullfunlem1  5887  fvfullfunlem2  5888  fvfullfunlem3  5889  clos1basesuc  5904  antisymex  5932  foundex  5934  extex  5935  frd  5942  extd  5943  antird  5948  antid  5949  frds  5955  weds  5958  po0  5959  ider  5963  ssetpov  5964  idssen  6061  fundmen  6064  xpassen  6077  enpw1lem1  6081  enpw1  6082  enmap2lem4  6086  enmap1lem4  6092  enprmaplem3  6098  enprmaplem5  6100  enprmaplem6  6101  nenpw1pwlem2  6105  mucex  6154  ncspw1eu  6180  ceex  6195  ce0addcnnul  6200  ce0nn  6201  el2c  6212  lecponc  6234  leconnnc  6239  dflec3  6242  tcfnex  6264  nclenn  6269  nnltp1c  6271  nmembers1lem1  6272  nncdiv3  6277  nnc3n3p1  6278  spacind  6287  nchoicelem3  6291  nchoicelem12  6300  nchoicelem17  6305  nchoicelem19  6307
  Copyright terms: Public domain W3C validator