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

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

(Instead of introducing weq 1479 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 1331. This lets us avoid overloading the  = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1479 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1331. 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 1331 1  wff  x  =  y
Colors of variables: wff set class
Syntax hints:    = wceq 1331
This theorem is referenced by:  alequcoms  1496  equidqe  1512  ax4sp1  1513  equid  1677  nfequid  1678  stdpc6  1679  equcomi  1680  ax6evr  1681  equcom  1682  equcomd  1683  equcoms  1684  equtr  1685  equtrr  1686  equtr2  1687  equequ1  1688  equequ2  1689  elequ1  1690  elequ2  1691  ax11i  1692  ax10o  1693  ax10  1695  nfae  1697  hbaes  1698  hbnae  1699  nfnae  1700  hbnaes  1701  equsalh  1704  equsal  1705  dral1  1708  dral2  1709  drex2  1710  drnf1  1711  drnf2  1712  spimth  1713  spimh  1715  spimed  1718  cbv1  1722  cbv1h  1723  cbv2h  1724  cbvalh  1726  chvar  1730  sbimi  1737  sb1  1739  sb2  1740  sbequ1  1741  sbequ2  1742  sbequ12  1744  sbequ12r  1745  sbequ12a  1746  sbid  1747  stdpc4  1748  sbh  1749  sb6x  1752  sbequ5  1755  sbequ6  1756  equsb1  1758  equsb2  1759  sbiedh  1760  sbiedv  1762  sbieh  1763  equs5a  1766  drsb1  1771  exdistrfor  1772  sb4a  1773  equs45f  1774  sb6f  1775  sb5f  1776  sb4e  1777  hbsb2a  1778  hbsb2e  1779  sbcof2  1782  aev  1784  ax16  1785  dveeq2  1787  dveeq2or  1788  ax11v2  1792  ax11a2  1793  ax11b  1798  equs5  1801  equs5or  1802  sb3  1803  sb4  1804  sb4or  1805  sb4b  1806  sb4bor  1807  hbsb2  1808  nfsb2or  1809  sbequi  1811  sbequ  1812  drsb2  1813  spsbe  1814  spsbim  1815  sbequ8  1819  sbidm  1823  sb5rf  1824  sb6rf  1825  ax16i  1830  spv  1832  speiv  1834  equvin  1835  a16g  1836  a16gb  1837  a16nf  1838  sb56  1857  sb6  1858  sb5  1859  sbnv  1860  sbanv  1861  sborv  1862  sbi1v  1863  sbi2v  1864  cbval2  1893  cbvex2  1894  cbvaldva  1900  cbvexdva  1901  cbvex4v  1902  cleljust  1910  hbs1  1911  hbsbv  1914  nfsbxy  1915  nfsbxyt  1916  equsb3  1924  sbco  1941  sbcocom  1943  sbcomxyyz  1945  elsb3  1951  elsb4  1952  sb9v  1953  2sb5  1958  2sb6  1959  sbcom2v  1960  sb6a  1963  2sb5rf  1964  2sb6rf  1965  dfsb7  1966  sb7f  1967  sb7af  1968  sb10f  1970  sbel2x  1973  sbalyz  1974  sbal1yz  1976  sbal1  1977  sbexyz  1978  exsb  1983  2exsb  1984  dvelimALT  1985  dvelimfv  1986  hbsb4t  1988  nfsb4t  1989  dvelimf  1990  dvelimdf  1991  dvelimor  1993  dveeq1  1994  sbal2  1997  euf  2004  eubidh  2005  eubid  2006  hbeu1  2009  nfeu1  2010  sb8eu  2012  nfeuv  2017  sb8euh  2022  eu1  2024  mo2n  2027  euex  2029  eumo0  2030  mo23  2040  mor  2041  modc  2042  eu2  2043  eu3h  2044  mo2r  2051  mo3h  2052  mo2dc  2054  mo4f  2059  eu4  2061  moim  2063  moimv  2065  moanim  2073  mopick  2077  2eu4  2092  euequ1  2094  exists1  2095  axext3  2122  axext4  2123  bm1.1  2124  eleq1w  2200  cleqh  2239  cbvab  2263  sbab  2267  nfcjust  2269  drnfc1  2298  drnfc2  2299  dvelimdc  2301  dvelimc  2302  nfcvf  2303  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvraldva2  2661  cbvrexdva2  2662  cbvraldva  2663  cbvrexdva  2664  cbvral2v  2665  cbvrex2v  2666  cbvral3v  2667  sbralie  2670  cbvrab  2684  vjust  2687  vex  2689  rr19.3v  2823  rr19.28v  2824  ralab2  2848  rexab2  2850  reu2  2872  reu6  2873  reu3  2874  rmo4  2877  reu4  2878  reu7  2879  reu8  2880  rmo3f  2881  rmo4f  2882  cdeqi  2894  cdeqri  2895  cdeqth  2896  cdeqnot  2897  cdeqal  2898  cdeqab  2899  cdeqim  2902  cdeqcv  2903  cdeqeq  2904  cdeqel  2905  nfccdeq  2907  sbsbc  2913  sbc8g  2916  sbcco2  2931  sbc5  2932  sbcralt  2985  sbcralg  2987  sbcreug  2989  rmo3  3000  cbvcsbw  3007  cbvcsb  3008  sbcel12g  3017  sbceqg  3018  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  difjust  3072  unjust  3074  injust  3076  dfss2f  3088  dfdif3  3186  dfnul3  3366  dfif3  3487  preq12bg  3700  eluniab  3748  elintab  3782  int0  3785  dfiunv2  3849  cbviun  3850  cbviin  3851  cbvdisj  3916  disjiun  3924  sndisj  3925  sbcbrg  3982  cbvmptf  4022  cbvmpt  4023  axsep2  4047  bm1.3ii  4049  nalset  4058  zfpow  4099  el  4102  dtruarb  4115  copsexg  4166  opelopabsb  4182  swopo  4228  pofun  4234  issod  4241  frind  4274  zfun  4356  ruv  4465  dtru  4475  dcextest  4495  tfisi  4501  findes  4517  relop  4689  dfdmf  4732  dfrnf  4780  resiexg  4864  dfres2  4871  opabresid  4872  mptresid  4873  imai  4895  issref  4921  intasym  4923  cnvi  4943  rnxpid  4973  cnvpom  5081  nfiota1  5090  cbviota  5093  sb8iota  5095  iotaval  5099  iotanul  5103  iota4  5106  csbiotag  5116  dffun2  5133  dffun4  5134  dffun5r  5135  dffun6f  5136  dffun4f  5139  sbcfung  5147  funopg  5157  funinsn  5172  funcnveq  5186  fun11  5190  fununi  5191  funcnvuni  5192  imain  5205  isarep2  5210  brprcneu  5414  fv2  5416  elfv  5419  fv3  5444  relelfvdm  5453  fvmpt2  5504  ralrnmpt  5562  rexrnmpt  5563  ffnfvf  5579  f1veqaeq  5670  dff13f  5671  fliftfuns  5699  cbvriota  5740  csbriotag  5742  acexmid  5773  oprabidlem  5802  cbvmpox  5849  cbvmpo  5850  cbvmpov  5851  mpofun  5873  abrexex2  6022  fmpoco  6113  f1o2ndf1  6125  poxp  6129  tposoprab  6177  tfrlem3-2d  6209  tfrlemi1  6229  tfr1onlemsucfn  6237  tfr1onlemaccex  6245  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  dcdifsnid  6400  fnsnsplitdc  6401  funresdfunsndc  6402  eqerlem  6460  qliftfuns  6513  eroveu  6520  cbvixp  6609  mptelixpg  6628  idssen  6671  xpf1o  6738  xpmapen  6744  findcard2d  6785  nnwetri  6804  fiintim  6817  snexxph  6838  fidcenumlemim  6840  fidcenumlemrk  6842  fidcenum  6844  supmoti  6880  isoti  6894  supisoti  6897  cnvti  6906  ordiso2  6920  ctssdccl  6996  finct  7001  cc1  7085  cc2  7087  ltsopi  7140  addpipqqs  7190  mulpipqqs  7193  archpr  7463  cauappcvgprlemlol  7467  cauappcvgprlemopu  7468  cauappcvgprlemupu  7469  cauappcvgprlemdisj  7471  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  cauappcvgprlemlim  7481  caucvgprlemlol  7490  caucvgprlemopu  7491  caucvgprlemupu  7492  caucvgprlemdisj  7494  caucvgprlemloc  7495  caucvgprlemcl  7496  caucvgprlemladdrl  7498  caucvgprprlemcbv  7507  caucvgprprlemopu  7519  caucvgprprlemclphr  7525  caucvgprprlemexbt  7526  suplocexprlemmu  7538  suplocexprlemdisj  7540  caucvgsrlembound  7614  caucvgsrlembnd  7621  suplocsrlem  7628  suplocsr  7629  peano1nnnn  7672  axcaucvglemres  7719  axpre-suploc  7722  negf1o  8156  lbreu  8715  lbinf  8718  suprubex  8721  suprlubex  8722  suprleubex  8724  1nn  8743  uzind4s  9397  uzind4s2  9398  indstr  9400  supinfneg  9402  infsupneg  9403  eqreznegel  9418  lbzbi  9420  exbtwnzlemex  10039  exbtwnz  10040  rebtwn2zlemstep  10042  rebtwn2z  10044  iseqovex  10241  iseqvalcbv  10242  seqvalcd  10244  seqovcd  10248  seq3f1olemqsum  10285  seq3f1olemp  10287  seq3f1oleml  10288  seq3distr  10298  faclbnd6  10502  fimaxq  10585  cvg1nlemres  10769  resqrexlemsqa  10808  resqrexlemex  10809  cau3lem  10898  fclim  11075  climeu  11077  cn1lem  11095  climcau  11128  climcvg1n  11131  summodclem3  11161  summodclem2a  11162  summodclem2  11163  summodc  11164  zsumdc  11165  fsum3  11168  isumz  11170  isumss2  11174  fsumsersdc  11176  fsum3ser  11178  fsumadd  11187  fsum2dlemstep  11215  fisumcom2  11219  isumshft  11271  cvgratz  11313  mertensabs  11318  prodfdivap  11328  cbvprod  11339  prodmodclem3  11356  prodmodclem2a  11357  prodmodclem2  11358  prodmodc  11359  odd2np1lem  11580  zsupcl  11651  infssuzex  11653  infssuzledc  11654  bezoutlemmain  11697  bezoutlemeu  11706  gcdmultiple  11719  rplpwr  11726  pw2dvdseu  11857  hashdvds  11908  ennnfonelemg  11927  ennnfoneleminc  11935  ennnfonelemkh  11936  ennnfonelemhf1o  11937  ennnfonelemex  11938  ennnfonelemhom  11939  ennnfonelemrnh  11940  ennnfonelemfun  11941  ennnfonelemdm  11944  ennnfonelemr  11947  ennnfone  11949  inffinp1  11953  ctinf  11954  strsetsid  12006  baspartn  12231  cnpnei  12402  txdis1cn  12461  cnmptid  12464  xmetxp  12690  cncfmptc  12765  cncfmptid  12766  dedekindeulemloc  12780  dedekindicclemloc  12789  ivthinclemlr  12798  ivthinclemur  12800  ivthinclemloc  12802  ivthdec  12805  spimd  13031  2spim  13032  ch2var  13033  bj-sbimedh  13037  bj-sbimeh  13038  cbvrald  13054  sumdc2  13065  bdth  13088  bdcdeq  13096  bdne  13110  bdreu  13112  bdcsn  13127  bdsep2  13143  bdsepnft  13144  bdsepnfALT  13146  bdbm1.3ii  13148  bj-nalset  13152  bj-zfpair2  13167  bj-bdfindes  13206  bj-nn0suc0  13207  bj-nntrans  13208  setindft  13222  setindis  13224  bdsetindis  13226  bj-inf2vnlem3  13229  bj-inf2vnlem4  13230  strcoll2  13240  strcollnft  13241  strcollnfALT  13243  sscoll2  13245  nnti  13250  nnsf  13260  peano4nninf  13261  nninfsellemqall  13272  nninfomni  13276  trilpolemeq1  13294
  Copyright terms: Public domain W3C validator