Theorem weq 1556

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

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

This proof depends on syntax axioms:   = wceq 1402

This theorem is used by:  alequcoms  1569  equidqe  1585  ax4sp1  1586  spimfv  1751  chvarfv  1752  equid  1753  nfequid  1754  stdpc6  1755  equcomi  1756  ax6evr  1757  equcom  1758  equcomd  1759  equcoms  1760  equtr  1761  equtrr  1762  equtr2  1763  equequ1  1764  equequ2  1765  ax11i  1766  ax10o  1767  ax10  1769  nfae  1771  hbaes  1772  hbnae  1773  nfnae  1774  hbnaes  1775  equsalh  1778  equsal  1779  dral1  1783  dral2  1784  drex2  1785  drnf1  1786  drnf2  1787  spimth  1788  spimh  1790  spimed  1793  cbv1  1798  cbv1h  1799  cbv1v  1800  cbv2h  1801  cbv2w  1803  cbvalv1  1804  cbvexv1  1805  cbvalh  1806  chvar  1810  sbimi  1817  sb1  1819  sb2  1820  sbequ1  1821  sbequ2  1822  sbequ12  1824  sbequ12r  1825  sbequ12a  1826  sbid  1827  stdpc4  1828  sbh  1829  sb6x  1832  sbequ5  1835  sbequ6  1836  equsb1  1838  equsb2  1839  sbiedh  1840  sbiedv  1842  sbieh  1843  equsalv  1846  equs5a  1847  drsb1  1852  exdistrfor  1853  sb4a  1854  equs45f  1855  sb6f  1856  sb5f  1857  sb4e  1858  hbsb2a  1859  hbsb2e  1860  sbcof2  1863  aev  1865  ax16  1866  dveeq2  1868  dveeq2or  1869  ax11v2  1873  ax11a2  1874  ax11b  1879  equs5  1882  equs5or  1883  sb3  1884  sb4  1885  sb4or  1886  sb4b  1887  sb4bor  1888  hbsb2  1889  nfsb2or  1890  sbequi  1892  sbequ  1893  drsb2  1894  spsbe  1895  spsbim  1896  sbequ8  1900  sbidm  1904  sb5rf  1905  sb6rf  1906  ax16i  1911  spv  1913  speiv  1915  equvin  1916  a16g  1917  a16gb  1918  a16nf  1919  equsv  1938  sb56  1940  sb6  1941  sb5  1942  sbnv  1943  sbanv  1944  sborv  1945  sbi1v  1946  sbi2v  1947  cbvalvw  1975  cbvexvw  1976  cbval2  1977  cbvex2  1978  cbvaldva  1984  cbvexdva  1985  cbvaldvaw  1986  cbval2vw  1988  cbvex2vw  1989  cbvex4v  1990  hbs1  1998  hbsbv  2001  nfsbxy  2002  nfsbxyt  2003  nfsbv  2007  equsb3  2011  sbco  2028  sbcocom  2030  sbcomxyyz  2032  sb9v  2038  2sb5  2043  2sb6  2044  sbcom2v  2045  sb6a  2048  2sb5rf  2049  2sb6rf  2050  dfsb7  2051  sb7f  2052  sb7af  2053  sb10f  2055  sbel2x  2058  sbalyz  2059  sbal1yz  2061  sbal1  2062  sbexyz  2063  exsb  2068  2exsb  2069  dvelimALT  2070  dvelimfv  2071  hbsb4t  2073  nfsb4t  2074  dvelimf  2075  dvelimdf  2076  dvelimor  2078  dveeq1  2079  sbal2  2080  euf  2091  eubidh  2092  eubid  2093  hbeu1  2096  nfeu1  2097  sb8eu  2099  nfeuv  2104  sb8euh  2109  eu1  2111  mo2n  2114  euex  2116  eumo0  2117  mo23  2128  mor  2129  modc  2130  eu2  2131  eu3h  2132  mo2r  2139  mo3h  2140  mo2dc  2142  mo4f  2147  eu4  2149  moim  2151  moimv  2153  moanim  2161  mopick  2165  2eu4  2180  euequ1  2182  exists1  2183  elequ1  2213  elequ2  2214  cleljust  2215  elsb1  2216  elsb2  2217  axext3  2221  axext4  2222  bm1.1  2223  eleq1w  2299  cleqh  2338  abbib  2356  cbvabw  2363  cbvab  2364  sbab  2368  nfcjust  2380  drnfc1  2409  drnfc2  2410  nfabdw  2411  dvelimdc  2413  dvelimc  2414  nfcvf  2415  cbvrmow  2735  cbvralfw  2775  cbvrexfw  2776  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralvw  2790  cbvrexvw  2791  cbvreuvw  2792  cbvraldva2  2793  cbvrexdva2  2794  cbvraldva  2795  cbvrexdva  2796  cbvral2vw  2797  cbvrex2vw  2798  cbvral2v  2799  cbvrex2v  2800  cbvral3v  2801  sbralie  2804  cbvrab  2819  vjust  2822  vex  2824  rr19.3v  2965  rr19.28v  2966  ralab2  2990  rexab2  2992  reu2  3014  reu6  3015  reu3  3016  rmo4  3019  reu4  3020  reu7  3021  reu8  3022  rmo3f  3023  rmo4f  3024  cdeqi  3036  cdeqri  3037  cdeqth  3038  cdeqnot  3039  cdeqal  3040  cdeqab  3041  cdeqim  3044  cdeqcv  3045  cdeqeq  3046  cdeqel  3047  nfccdeq  3049  sbsbc  3055  sbc8g  3059  sbcco2  3074  sbc5  3075  sbcralt  3128  sbcralg  3130  sbcreug  3132  reu8nf  3133  rmo3  3144  cbvcsbw  3151  cbvcsb  3152  csbcow  3158  sbcel12g  3162  sbceqg  3163  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  difjust  3221  unjust  3223  injust  3225  dfssf  3238  dfss2f  3239  dfdif3  3339  dfnul2  3523  dfif3  3654  rabsnifsb  3777  preq12bg  3898  eluniab  3947  elintab  3981  int0  3984  dfiunv2  4048  cbviun  4049  cbviin  4050  cbvdisj  4116  invdisjrab  4124  disjiun  4125  sndisj  4126  sbcbrg  4185  cbvmptf  4225  cbvmpt  4226  axsepg  4250  bm1.3ii  4254  nalset  4263  zfpow  4312  el  4315  dtruarb  4328  copsexg  4384  opelopabsb  4402  swopo  4451  pofun  4457  issod  4464  frind  4497  zfun  4579  ruv  4697  dtru  4707  dcextest  4728  tfisi  4734  findes  4750  relop  4930  dfdmf  4974  dfrnf  5023  resiexg  5108  dfres2  5115  opabresid  5116  mptresid  5117  imai  5143  issref  5170  intasym  5172  cnvi  5192  rnxpid  5222  cnvpom  5330  nfiota1  5339  cbviota  5342  sb8iota  5345  iotaval  5349  iotanul  5353  iota4  5357  eliota  5365  eliotaeu  5366  csbiotag  5370  dffun2  5387  dffun4  5388  dffun5r  5389  dffun6f  5390  dffun4f  5393  sbcfung  5401  funopg  5411  fundif  5425  funinsn  5430  funcnveq  5444  fun11  5448  fununi  5449  funcnvuni  5450  imain  5463  isarep2  5468  brprcneu  5688  fv2  5690  elfv  5693  fv3  5718  relelfvdm  5727  fvmpt2  5789  ralrnmpt  5850  rexrnmpt  5851  ffnfvf  5867  f1veqaeq  5975  dff13f  5976  fliftfuns  6004  canth  6036  cbvriotavw  6049  cbvriota  6050  csbriotag  6052  acexmid  6084  oprabidlem  6116  cbvmpox  6166  cbvmpo  6167  cbvmpov  6168  mpofun  6190  abrexex2  6353  fmpoco  6452  f1o2ndf1  6464  poxp  6468  suppfnss  6497  tposoprab  6551  tfrlem3-2d  6583  tfrlemi1  6603  tfr1onlemsucfn  6611  tfr1onlemaccex  6619  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  dcdifsnid  6777  fnsnsplitdc  6778  funresdfunsndc  6779  eqerlem  6838  qliftfuns  6893  eroveu  6900  cbvixp  6997  mptelixpg  7016  idssen  7063  modom  7108  pw2f1odclem  7134  xpf1o  7144  xpmapen  7150  findcard2d  7195  fidcen  7203  eqsndc  7210  nnwetri  7223  fiintim  7238  snexxph  7267  fidcenumlemim  7269  fidcenumlemrk  7271  fidcenum  7273  2omap  7319  supmoti  7334  isoti  7348  supisoti  7351  cnvti  7360  ordiso2  7376  ctssdccl  7452  finct  7457  infnninf  7465  nninfwlpoim  7520  nninfwlpo  7522  sspw1or2  7545  exmidontriimlem3  7580  exmidontriimlem4  7581  exmidontriim  7582  onntri13  7598  onntri51  7600  onntri3or  7605  tapap  7617  dftap2  7618  netap  7621  2onetap  7622  2omotaplemap  7624  cc1  7632  cc2  7634  ltsopi  7688  addpipqqs  7738  mulpipqqs  7741  archpr  8011  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlemlim  8029  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdrl  8046  caucvgprprlemcbv  8055  caucvgprprlemopu  8067  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  suplocexprlemmu  8086  suplocexprlemdisj  8088  caucvgsrlembound  8162  caucvgsrlembnd  8169  suplocsrlem  8176  suplocsr  8177  peano1nnnn  8220  axcaucvglemres  8267  axpre-suploc  8270  negf1o  8711  lbreu  9278  lbinf  9281  suprubex  9284  suprlubex  9285  suprleubex  9287  1nn  9318  zfidc  9728  uzind4s  10000  uzind4s2  10001  indstr  10003  supinfneg  10005  infsupneg  10006  infregelbex  10008  eqreznegel  10024  lbzbi  10026  elpq  10060  zsupcl  10675  infssuzex  10677  infssuzledc  10678  zsupssdc  10684  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  iseqovex  10909  iseqvalcbv  10910  seqvalcd  10912  seqovcd  10918  seq3f1olemqsum  10964  seq3f1olemp  10966  seq3f1oleml  10967  seqf1og  10972  seq3distr  10983  faclbnd6  11197  fimaxq  11285  hashfibclem  11297  hashf1lem1  11300  wrd2ind  11510  reuccatpfxs1lem  11533  reuccatpfxs1  11534  cvg1nlemres  11766  resqrexlemsqa  11805  resqrexlemex  11806  cau3lem  11896  fclim  12078  climeu  12080  cn1lem  12098  climcau  12131  climcvg1n  12134  summodclem3  12165  summodclem2a  12166  summodclem2  12167  summodc  12168  zsumdc  12169  fsum3  12172  isumz  12174  isumss2  12178  fsumsersdc  12180  fsum3ser  12182  fsumadd  12191  fsum2dlemstep  12219  fisumcom2  12223  isumshft  12275  cvgratz  12317  mertensabs  12322  prodfdivap  12332  cbvprod  12343  prodmodclem3  12360  prodmodclem2a  12361  prodmodclem2  12362  prodmodc  12363  zproddc  12364  fprodseq  12368  fprodm1s  12386  fprodp1s  12387  fprod2dlemstep  12407  fprodcom2fi  12411  fprodsplitf  12417  odd2np1lem  12657  bitsfzolem  12739  bezoutlemmain  12793  bezoutlemeu  12802  gcdmultiple  12815  rplpwr  12822  nnwofdc  12833  nnwosdc  12834  nninfctlemfo  12835  isprm5lem  12938  isprm5  12939  pwbdvdseu  12965  hashdvds  13021  eulerthlemh  13031  reumodprminv  13054  pclemub  13088  pclemdc  13089  pceu  13096  pcmptdvds  13146  1arith  13168  4sqlem2  13190  4sqlem11  13202  4sqlem12  13203  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemefi  13288  ballotfilemodife  13291  ennnfonelemg  13345  ennnfoneleminc  13353  ennnfonelemkh  13354  ennnfonelemhf1o  13355  ennnfonelemex  13356  ennnfonelemhom  13357  ennnfonelemrnh  13358  ennnfonelemfun  13359  ennnfonelemdm  13362  ennnfonelemr  13365  ennnfone  13367  inffinp1  13371  ctinf  13372  nninfdclemf  13391  nninfdclemp1  13392  unbendc  13396  infpn2  13398  strsetsid  13436  mgmidmo  13743  lidrididd  13753  mndinvmod  13809  insubm  13843  dfgrp3mlem  13954  mulgaddcom  14000  mulginvcom  14001  isnsg2  14057  gzsumconstf  14195  srgmulgass  14344  islmodd  14680  lmodvsmmulgdi  14711  rmodislmodlem  14738  rmodislmod  14739  lssats2  14802  assamulgscm  15094  mplsubgfilemcl  15142  baspartn  15203  cnpnei  15372  txdis1cn  15431  cnmptid  15434  xmetxp  15660  cncfmptc  15749  cncfmptid  15750  dedekindeulemloc  15772  dedekindicclemloc  15781  ivthinclemlr  15790  ivthinclemur  15792  ivthinclemloc  15794  ivthdec  15797  dvmptfsum  15878  plymullem1  15901  zprmlogbap  16140  perfectlem2  16222  bposlem5  16237  lgseisenlem2  16312  lgsquadlem3  16320  lgsquad  16321  lgsquad2lem2  16323  2lgslem1a  16329  usgruspgrben  16549  umgr2edg1  16572  umgr2edgneu  16575  usgredg4  16578  usgredgreu  16579  uspgredg2vtxeu  16581  vtxedgfi  16652  vtxlpfi  16653  depindlem1  16869  depindlem2  16870  depindlem3  16871  spimd  16915  2spim  16916  ch2var  16917  bj-sbimedh  16921  bj-sbimeh  16922  cbvrald  16938  sumdc2  16949  bdth  16979  bdcdeq  16987  bdne  17001  bdreu  17003  bdcsn  17018  bdsep2  17034  bdsepnft  17035  bdsepnfALT  17037  bdbm1.3ii  17039  bj-nalset  17043  bj-zfpair2  17058  bj-bdfindes  17097  bj-nn0suc0  17098  bj-nntrans  17099  setindft  17113  setindis  17115  bdsetindis  17117  bj-inf2vnlem3  17120  bj-inf2vnlem4  17121  strcoll2  17131  strcollnft  17132  strcollnfALT  17134  sscoll2  17136  nnti  17144  nnsf  17170  peano4nninf  17171  nninfsellemqall  17180  nninfomni  17184  nnnninfen  17186  repiecef  17199  trilpolemeq1  17211  tridceq  17228  redc0  17229  reap0  17230  dceqnconst  17232  dcapnconst  17233  nconstwlpolemgt0  17236  cbvals  17268