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

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

(Instead of introducing weq 1399 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 1398. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1399 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1398. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.)

Assertion
Ref Expression
weq

Proof of Theorem weq
StepHypRef Expression
1 wceq 1398 1
Colors of variables: wff set class
Syntax hints:   wceq 1398
This theorem is referenced by:  hbequid  1408  alequcoms  1410  nalequcoms  1411  equs3  1412  a9wa9lem1  1415  a9wa9lem2  1416  a9wa9lem3  1417  a9wa9lem8  1422  a9wa9  1423  equidqe  1425  equidq  1426  ax4sp1  1427  ax4  1428  ax9o  1518  ax9  1520  a9e  1521  equid  1522  equidALT  1523  equid1  1524  stdpc6  1525  equcomi  1526  equcom  1527  equcoms  1528  equtr  1529  equtrr  1530  equtr2  1531  equequ1  1532  equequ2  1533  elequ1  1534  elequ2  1535  ax11i  1536  ax10o  1537  ax10  1539  hbae  1540  hbaes  1541  hbnae  1542  hbnaes  1543  equsal  1545  equsex  1546  dvelimfALT  1547  dral1  1548  dral2  1549  drex1  1550  drex2  1551  exdistrf  1552  a4imt  1553  a4im  1554  a4ime  1555  a4imed  1556  cbv1  1557  cbv2  1558  cbv3  1559  cbv3ALT  1560  cbval  1561  cbvex  1562  chvar  1563  equvini  1564  equveli  1565  sbimi  1569  drsb1  1571  sb1  1572  sb2  1573  sbequ1  1574  sbequ2  1575  sbequ12  1577  sbequ12r  1578  sbequ12a  1579  sbid  1580  stdpc4  1581  sbf  1582  sbequ5  1586  sbequ6  1587  equsb1  1589  equsb2  1590  sbied  1591  sbie  1592  equs5a  1593  equs5e  1594  sb4a  1595  equs45f  1596  sb6f  1597  sb5f  1598  sb4e  1599  hbsb2a  1600  hbsb2e  1601  aev  1604  ax16  1605  ax17eq  1607  dveeq2  1608  dveeq2ALT  1609  ax11v2  1613  ax11a2  1614  ax11  1617  ax11b  1618  equs5  1619  sb3  1620  sb4  1621  sb4b  1622  dfsb2  1623  dfsb3  1624  hbsb2  1625  sbequi  1626  sbequ  1627  sbn  1629  sbi1  1630  sbequ8  1646  hbsb4  1648  hbsb4t  1649  dvelimf  1650  dvelimdf  1651  sbco  1652  sbidm  1654  sbco2  1655  sbco3  1657  sbcom  1658  sb5rf  1659  sb6rf  1660  sb9i  1663  ax11v  1665  sb56  1666  sb6  1667  sb5  1668  ax16i  1669  a4v  1671  a4eiv  1673  equvin  1674  a16g  1675  a16gb  1676  cbval2  1719  cbvex2  1720  cbvexd  1724  cbvex4v  1725  cleljust  1732  equsb3  1734  elsb3  1735  elsb4  1736  hbs1  1737  hbsb  1740  2sb5  1742  2sb6  1743  sbcom2  1744  sb6a  1746  2sb5rf  1747  2sb6rf  1748  dfsb7  1749  sb7f  1750  sb10f  1751  sbelx  1753  sbel2x  1754  sbal1  1755  sbal  1756  exsb  1759  2exsb  1760  dvelimALT  1762  dveeq1  1763  dveeq1ALT  1764  sbal2  1767  ax15  1768  ax17el  1770  ax11eq  1772  ax11el  1773  ax11f  1774  ax11indn  1775  ax11indi  1776  ax11indalem  1777  ax11inda2ALT  1778  ax11inda2  1779  ax11inda  1780  a12stdy1  1781  a12stdy2  1782  a12stdy3  1783  a12stdy4  1784  a12lem1  1785  a12lem2  1786  a12study  1787  a12studyALT  1788  a12study3  1790  eujustALT  1794  euf  1797  eubid  1798  eubii  1800  hbeu1  1801  hbeu  1802  eu1  1806  mo  1807  euex  1808  eumo0  1809  eu2  1810  eu3  1811  mo2  1814  mo3  1816  mo4f  1817  mobii  1820  eu5  1824  eu4  1825  immo  1832  moimv  1834  moanim  1842  mopick  1848  2mo  1864  2mos  1865  2eu4  1869  2eu5  1870  2eu6  1871  euequ1  1874  exists1  1875  cbvrex2v  2288  ninjust  2612  csbing  2725  dfnul2  2728  sneqbg  2852  euabsn  3010  dfif3  3117  csbifg  3134  axxpprim  3192  axcnvprim  3193  axssetprim  3194  axsiprim  3195  axtyplowerprim  3196  axins2prim  3197  axins3prim  3198  snex  3213  pwadjoin  3221  preqr2g  3228  preq12bg  3232  1cex  3246  opkabssvvk  3312  sikss1c1c  3371  opkelidkg  3378  idkssvvk  3385  dfpw12  3405  dfidk2  3417  unipw1  3435  eqpw1uni  3440  dfeu2  3443  peano2  3511  addcid1  3513  nnc0suc  3519  nncaddccl  3526  nnsucelrlem1  3531  nnsucelr  3535  nndisjeq  3536  preaddccan1lem1  3561  preaddccan1  3562  ltfintrilem1  3573  ltfintri  3574  ssfin  3578  vfinnc  3579  ncfinraise  3589  ncfinlower  3591  nnpw1ex  3592  eqtfinrelk  3594  oddfinex  3612  evenoddnnnul  3622  evenodddisjlem1  3623  evenodddisj  3624  nnadjoinlem1  3627  nnadjoin  3628  nnadjoinpw  3629  nnpweq  3631  sfindbl  3638  sfintfin  3640  tfinnn  3642  spfinsfincl  3647  vfinspsslem1  3658  vfinspss  3659  vfinspclt  3660  dfphi2  3677  phi11lem1  3701  proj1op  3706  proj2op  3707  copsexg  3713  phidisjnn  3721  cbvopab  3727  sbcbrg  3782  opelopabsb  3795  br1stg  3828  dfima2  3843  dfco1  3846  dfsi2  3849  ralxpf  3993  ideqg  4059  ideqg2  4060  dmi  4110  csbima12g  4147  iss  4193  dfres2  4195  opabresid  4196  intasym  4224  intirr  4225  coi1  4300  dfxp2  4323  dffun2  4329  nfunv  4349  funun  4357  fun11iun  4521  fv2  4540  elfv  4542  csbfv12g  4553  fv3  4558  tz6.12f  4563  tz6.12-2  4564  dffn5  4581  fvopab4gf  4608  fvopabgf  4614  fvopabnf  4615  fnasrn  4649  fvi  4682  fconstfv  4696  dff13  4711  isotr  4737  dfid4  4746  1stfo  4748  2ndfo  4749  swapf1o  4754  fununiq  4760  funsi  4764  oprabid  4787  csbovg  4789  cbvoprab12  4806  ov2gf  4837  cbvmpt  4918  fvmpt2i  4940  mptresid  4955  trtxp  5000  brtxp  5002  elfix  5007  oqelins4  5014  fntxp  5025  addcfnex  5043  funsex  5047  qrpprod  5051  dmpprod  5057  fnpprod  5060  pw1fnf1o  5072  fnfullfunlem1  5073  fnfullfunlem2  5074  fvfullfunlem1  5078  fvfullfunlem2  5079  fvfullfunlem3  5080  clos1basesuc  5095  antisymex  5123  foundex  5125  extex  5126  frd  5133  extd  5134  antird  5139  antid  5140  frds  5146  weds  5149  po0  5150  ider  5154  ssetpov  5155  idssen  5253  fundmen  5256  xpassen  5269  enpw1lem1  5273  enpw1  5274  enmap2lem4  5278  enmap1lem4  5284  enprmaplem3  5290  enprmaplem5  5292  enprmaplem6  5293  nenpw1pwlem2  5297  mucex  5346  ncspw1eu  5372  ceex  5387  ce0addcnnul  5392  ce0nn  5393  el2c  5404  lecponc  5426  leconnnc  5431  dflec3  5434  tcfnex  5456  nclenn  5461  nnltp1c  5463  nmembers1lem1  5464  nncdiv3  5469  nnc3n3p1  5470  spacind  5479  nchoicelem3  5483  nchoicelem12  5492  nchoicelem17  5497  nchoicelem19  5499  eq0cprim  5501  elsucprim  5502  eqsucprim  5503  elnncprim  5504  elphiprim  5505  elopprim  5506
  Copyright terms: Public domain W3C validator