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 𝑥 = 𝑦

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1331	1 wff 𝑥 = 𝑦

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  1891  cbvex2  1892  cbvaldva  1898  cbvexdva  1899  cbvex4v  1900  cleljust  1908  hbs1  1909  hbsbv  1912  nfsbxy  1913  nfsbxyt  1914  equsb3  1922  sbco  1939  sbcocom  1941  sbcomxyyz  1943  elsb3  1949  elsb4  1950  sb9v  1951  2sb5  1956  2sb6  1957  sbcom2v  1958  sb6a  1961  2sb5rf  1962  2sb6rf  1963  dfsb7  1964  sb7f  1965  sb7af  1966  sb10f  1968  sbel2x  1971  sbalyz  1972  sbal1yz  1974  sbal1  1975  sbexyz  1976  exsb  1981  2exsb  1982  dvelimALT  1983  dvelimfv  1984  hbsb4t  1986  nfsb4t  1987  dvelimf  1988  dvelimdf  1989  dvelimor  1991  dveeq1  1992  sbal2  1995  euf  2002  eubidh  2003  eubid  2004  hbeu1  2007  nfeu1  2008  sb8eu  2010  nfeuv  2015  sb8euh  2020  eu1  2022  mo2n  2025  euex  2027  eumo0  2028  mo23  2038  mor  2039  modc  2040  eu2  2041  eu3h  2042  mo2r  2049  mo3h  2050  mo2dc  2052  mo4f  2057  eu4  2059  moim  2061  moimv  2063  moanim  2071  mopick  2075  2eu4  2090  euequ1  2092  exists1  2093  axext3  2120  axext4  2121  bm1.1  2122  eleq1w  2198  cleqh  2237  cbvab  2261  sbab  2265  nfcjust  2267  drnfc1  2296  drnfc2  2297  dvelimdc  2299  dvelimc  2300  nfcvf  2301  cbvralf  2646  cbvrexf  2647  cbvreu  2650  cbvraldva2  2656  cbvrexdva2  2657  cbvraldva  2658  cbvrexdva  2659  cbvral2v  2660  cbvrex2v  2661  cbvral3v  2662  sbralie  2665  cbvrab  2679  vjust  2682  vex  2684  rr19.3v  2818  rr19.28v  2819  ralab2  2843  rexab2  2845  reu2  2867  reu6  2868  reu3  2869  rmo4  2872  reu4  2873  reu7  2874  reu8  2875  rmo3f  2876  rmo4f  2877  cdeqi  2889  cdeqri  2890  cdeqth  2891  cdeqnot  2892  cdeqal  2893  cdeqab  2894  cdeqim  2897  cdeqcv  2898  cdeqeq  2899  cdeqel  2900  nfccdeq  2902  sbsbc  2908  sbc8g  2911  sbcco2  2926  sbc5  2927  sbcralt  2980  sbcralg  2982  sbcreug  2984  rmo3  2995  cbvcsbw  3002  cbvcsb  3003  sbcel12g  3012  sbceqg  3013  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  difjust  3067  unjust  3069  injust  3071  dfss2f  3083  dfdif3  3181  dfnul3  3361  dfif3  3482  preq12bg  3695  eluniab  3743  elintab  3777  int0  3780  dfiunv2  3844  cbviun  3845  cbviin  3846  cbvdisj  3911  disjiun  3919  sndisj  3920  sbcbrg  3977  cbvmptf  4017  cbvmpt  4018  axsep2  4042  bm1.3ii  4044  nalset  4053  zfpow  4094  el  4097  dtruarb  4110  copsexg  4161  opelopabsb  4177  swopo  4223  pofun  4229  issod  4236  frind  4269  zfun  4351  ruv  4460  dtru  4470  dcextest  4490  tfisi  4496  findes  4512  relop  4684  dfdmf  4727  dfrnf  4775  resiexg  4859  dfres2  4866  opabresid  4867  mptresid  4868  imai  4890  issref  4916  intasym  4918  cnvi  4938  rnxpid  4968  cnvpom  5076  nfiota1  5085  cbviota  5088  sb8iota  5090  iotaval  5094  iotanul  5098  iota4  5101  csbiotag  5111  dffun2  5128  dffun4  5129  dffun5r  5130  dffun6f  5131  dffun4f  5134  sbcfung  5142  funopg  5152  funinsn  5167  funcnveq  5181  fun11  5185  fununi  5186  funcnvuni  5187  imain  5200  isarep2  5205  brprcneu  5407  fv2  5409  elfv  5412  fv3  5437  relelfvdm  5446  fvmpt2  5497  ralrnmpt  5555  rexrnmpt  5556  ffnfvf  5572  f1veqaeq  5663  dff13f  5664  fliftfuns  5692  cbvriota  5733  csbriotag  5735  acexmid  5766  oprabidlem  5795  cbvmpox  5842  cbvmpo  5843  cbvmpov  5844  mpofun  5866  abrexex2  6015  fmpoco  6106  f1o2ndf1  6118  poxp  6122  tposoprab  6170  tfrlem3-2d  6202  tfrlemi1  6222  tfr1onlemsucfn  6230  tfr1onlemaccex  6238  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemaccex  6251  dcdifsnid  6393  fnsnsplitdc  6394  funresdfunsndc  6395  eqerlem  6453  qliftfuns  6506  eroveu  6513  cbvixp  6602  mptelixpg  6621  idssen  6664  xpf1o  6731  xpmapen  6737  findcard2d  6778  nnwetri  6797  fiintim  6810  snexxph  6831  fidcenumlemim  6833  fidcenumlemrk  6835  fidcenum  6837  supmoti  6873  isoti  6887  supisoti  6890  cnvti  6899  ordiso2  6913  ctssdccl  6989  finct  6994  ltsopi  7121  addpipqqs  7171  mulpipqqs  7174  archpr  7444  cauappcvgprlemlol  7448  cauappcvgprlemopu  7449  cauappcvgprlemupu  7450  cauappcvgprlemdisj  7452  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlemlim  7462  caucvgprlemlol  7471  caucvgprlemopu  7472  caucvgprlemupu  7473  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprlemcl  7477  caucvgprlemladdrl  7479  caucvgprprlemcbv  7488  caucvgprprlemopu  7500  caucvgprprlemclphr  7506  caucvgprprlemexbt  7507  suplocexprlemmu  7519  suplocexprlemdisj  7521  caucvgsrlembound  7595  caucvgsrlembnd  7602  suplocsrlem  7609  suplocsr  7610  peano1nnnn  7653  axcaucvglemres  7700  axpre-suploc  7703  negf1o  8137  lbreu  8696  lbinf  8699  suprubex  8702  suprlubex  8703  suprleubex  8705  1nn  8724  uzind4s  9378  uzind4s2  9379  indstr  9381  supinfneg  9383  infsupneg  9384  eqreznegel  9399  lbzbi  9401  exbtwnzlemex  10020  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  iseqovex  10222  iseqvalcbv  10223  seqvalcd  10225  seqovcd  10229  seq3f1olemqsum  10266  seq3f1olemp  10268  seq3f1oleml  10269  seq3distr  10279  faclbnd6  10483  fimaxq  10566  cvg1nlemres  10750  resqrexlemsqa  10789  resqrexlemex  10790  cau3lem  10879  fclim  11056  climeu  11058  cn1lem  11076  climcau  11109  climcvg1n  11112  summodclem3  11142  summodclem2a  11143  summodclem2  11144  summodc  11145  zsumdc  11146  fsum3  11149  isumz  11151  isumss2  11155  fsumsersdc  11157  fsum3ser  11159  fsumadd  11168  fsum2dlemstep  11196  fisumcom2  11200  isumshft  11252  cvgratz  11294  mertensabs  11299  prodfdivap  11309  cbvprod  11320  odd2np1lem  11558  zsupcl  11629  infssuzex  11631  infssuzledc  11632  bezoutlemmain  11675  bezoutlemeu  11684  gcdmultiple  11697  rplpwr  11704  pw2dvdseu  11835  hashdvds  11886  ennnfonelemg  11905  ennnfoneleminc  11913  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemrnh  11918  ennnfonelemfun  11919  ennnfonelemdm  11922  ennnfonelemr  11925  ennnfone  11927  inffinp1  11931  ctinf  11932  strsetsid  11981  baspartn  12206  cnpnei  12377  txdis1cn  12436  cnmptid  12439  xmetxp  12665  cncfmptc  12740  cncfmptid  12741  dedekindeulemloc  12755  dedekindicclemloc  12764  ivthinclemlr  12773  ivthinclemur  12775  ivthinclemloc  12777  ivthdec  12780  spimd  12961  2spim  12962  ch2var  12963  bj-sbimedh  12967  bj-sbimeh  12968  cbvrald  12984  sumdc2  12995  bdth  13018  bdcdeq  13026  bdne  13040  bdreu  13042  bdcsn  13057  bdsep2  13073  bdsepnft  13074  bdsepnfALT  13076  bdbm1.3ii  13078  bj-nalset  13082  bj-zfpair2  13097  bj-bdfindes  13136  bj-nn0suc0  13137  bj-nntrans  13138  setindft  13152  setindis  13154  bdsetindis  13156  bj-inf2vnlem3  13159  bj-inf2vnlem4  13160  strcoll2  13170  strcollnft  13171  strcollnfALT  13173  sscoll2  13175  nnti  13180  nnsf  13188  peano4nninf  13189  nninfsellemqall  13200  nninfomni  13204  trilpolemeq1  13222