Theorem weq 1549

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

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

Syntax hints:   = wceq 1395

This theorem is referenced by:  alequcoms  1562  equidqe  1578  ax4sp1  1579  spimfv  1745  chvarfv  1746  equid  1747  nfequid  1748  stdpc6  1749  equcomi  1750  ax6evr  1751  equcom  1752  equcomd  1753  equcoms  1754  equtr  1755  equtrr  1756  equtr2  1757  equequ1  1758  equequ2  1759  ax11i  1760  ax10o  1761  ax10  1763  nfae  1765  hbaes  1766  hbnae  1767  nfnae  1768  hbnaes  1769  equsalh  1772  equsal  1773  dral1  1776  dral2  1777  drex2  1778  drnf1  1779  drnf2  1780  spimth  1781  spimh  1783  spimed  1786  cbv1  1791  cbv1h  1792  cbv1v  1793  cbv2h  1794  cbv2w  1796  cbvalv1  1797  cbvexv1  1798  cbvalh  1799  chvar  1803  sbimi  1810  sb1  1812  sb2  1813  sbequ1  1814  sbequ2  1815  sbequ12  1817  sbequ12r  1818  sbequ12a  1819  sbid  1820  stdpc4  1821  sbh  1822  sb6x  1825  sbequ5  1828  sbequ6  1829  equsb1  1831  equsb2  1832  sbiedh  1833  sbiedv  1835  sbieh  1836  equsalv  1839  equs5a  1840  drsb1  1845  exdistrfor  1846  sb4a  1847  equs45f  1848  sb6f  1849  sb5f  1850  sb4e  1851  hbsb2a  1852  hbsb2e  1853  sbcof2  1856  aev  1858  ax16  1859  dveeq2  1861  dveeq2or  1862  ax11v2  1866  ax11a2  1867  ax11b  1872  equs5  1875  equs5or  1876  sb3  1877  sb4  1878  sb4or  1879  sb4b  1880  sb4bor  1881  hbsb2  1882  nfsb2or  1883  sbequi  1885  sbequ  1886  drsb2  1887  spsbe  1888  spsbim  1889  sbequ8  1893  sbidm  1897  sb5rf  1898  sb6rf  1899  ax16i  1904  spv  1906  speiv  1908  equvin  1909  a16g  1910  a16gb  1911  a16nf  1912  sb56  1932  sb6  1933  sb5  1934  sbnv  1935  sbanv  1936  sborv  1937  sbi1v  1938  sbi2v  1939  cbvalvw  1966  cbvexvw  1967  cbval2  1968  cbvex2  1969  cbvaldva  1975  cbvexdva  1976  cbvaldvaw  1977  cbval2vw  1979  cbvex2vw  1980  cbvex4v  1981  hbs1  1989  hbsbv  1992  nfsbxy  1993  nfsbxyt  1994  nfsbv  1998  equsb3  2002  sbco  2019  sbcocom  2021  sbcomxyyz  2023  sb9v  2029  2sb5  2034  2sb6  2035  sbcom2v  2036  sb6a  2039  2sb5rf  2040  2sb6rf  2041  dfsb7  2042  sb7f  2043  sb7af  2044  sb10f  2046  sbel2x  2049  sbalyz  2050  sbal1yz  2052  sbal1  2053  sbexyz  2054  exsb  2059  2exsb  2060  dvelimALT  2061  dvelimfv  2062  hbsb4t  2064  nfsb4t  2065  dvelimf  2066  dvelimdf  2067  dvelimor  2069  dveeq1  2070  sbal2  2071  euf  2082  eubidh  2083  eubid  2084  hbeu1  2087  nfeu1  2088  sb8eu  2090  nfeuv  2095  sb8euh  2100  eu1  2102  mo2n  2105  euex  2107  eumo0  2108  mo23  2119  mor  2120  modc  2121  eu2  2122  eu3h  2123  mo2r  2130  mo3h  2131  mo2dc  2133  mo4f  2138  eu4  2140  moim  2142  moimv  2144  moanim  2152  mopick  2156  2eu4  2171  euequ1  2173  exists1  2174  elequ1  2204  elequ2  2205  cleljust  2206  elsb1  2207  elsb2  2208  axext3  2212  axext4  2213  bm1.1  2214  eleq1w  2290  cleqh  2329  cbvabw  2352  cbvab  2353  sbab  2357  nfcjust  2360  drnfc1  2389  drnfc2  2390  nfabdw  2391  dvelimdc  2393  dvelimc  2394  nfcvf  2395  cbvrmow  2714  cbvralfw  2754  cbvrexfw  2755  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvralvw  2769  cbvrexvw  2770  cbvreuvw  2771  cbvraldva2  2772  cbvrexdva2  2773  cbvraldva  2774  cbvrexdva  2775  cbvral2vw  2776  cbvrex2vw  2777  cbvral2v  2778  cbvrex2v  2779  cbvral3v  2780  sbralie  2783  cbvrab  2797  vjust  2800  vex  2802  rr19.3v  2942  rr19.28v  2943  ralab2  2967  rexab2  2969  reu2  2991  reu6  2992  reu3  2993  rmo4  2996  reu4  2997  reu7  2998  reu8  2999  rmo3f  3000  rmo4f  3001  cdeqi  3013  cdeqri  3014  cdeqth  3015  cdeqnot  3016  cdeqal  3017  cdeqab  3018  cdeqim  3021  cdeqcv  3022  cdeqeq  3023  cdeqel  3024  nfccdeq  3026  sbsbc  3032  sbc8g  3036  sbcco2  3051  sbc5  3052  sbcralt  3105  sbcralg  3107  sbcreug  3109  reu8nf  3110  rmo3  3121  cbvcsbw  3128  cbvcsb  3129  csbcow  3135  sbcel12g  3139  sbceqg  3140  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  difjust  3198  unjust  3200  injust  3202  dfss2f  3215  dfdif3  3314  dfnul3  3494  dfif3  3616  preq12bg  3850  eluniab  3899  elintab  3933  int0  3936  dfiunv2  4000  cbviun  4001  cbviin  4002  cbvdisj  4068  invdisjrab  4076  disjiun  4077  sndisj  4078  sbcbrg  4137  cbvmptf  4177  cbvmpt  4178  axsep2  4202  bm1.3ii  4204  nalset  4213  zfpow  4258  el  4261  dtruarb  4274  copsexg  4329  opelopabsb  4347  swopo  4394  pofun  4400  issod  4407  frind  4440  zfun  4522  ruv  4639  dtru  4649  dcextest  4670  tfisi  4676  findes  4692  relop  4869  dfdmf  4913  dfrnf  4961  resiexg  5046  dfres2  5053  opabresid  5054  mptresid  5055  imai  5080  issref  5107  intasym  5109  cnvi  5129  rnxpid  5159  cnvpom  5267  nfiota1  5276  cbviota  5279  sb8iota  5282  iotaval  5286  iotanul  5290  iota4  5294  eliota  5302  eliotaeu  5303  csbiotag  5307  dffun2  5324  dffun4  5325  dffun5r  5326  dffun6f  5327  dffun4f  5330  sbcfung  5338  funopg  5348  fundif  5361  funinsn  5366  funcnveq  5380  fun11  5384  fununi  5385  funcnvuni  5386  imain  5399  isarep2  5404  brprcneu  5616  fv2  5618  elfv  5621  fv3  5646  relelfvdm  5655  fvmpt2  5711  ralrnmpt  5770  rexrnmpt  5771  ffnfvf  5787  f1veqaeq  5886  dff13f  5887  fliftfuns  5915  canth  5945  cbvriotavw  5958  cbvriota  5959  csbriotag  5961  acexmid  5993  oprabidlem  6025  cbvmpox  6073  cbvmpo  6074  cbvmpov  6075  mpofun  6097  abrexex2  6259  fmpoco  6352  f1o2ndf1  6364  poxp  6368  tposoprab  6416  tfrlem3-2d  6448  tfrlemi1  6468  tfr1onlemsucfn  6476  tfr1onlemaccex  6484  tfrcllemsucfn  6489  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllembfn  6493  tfrcllemaccex  6497  dcdifsnid  6640  fnsnsplitdc  6641  funresdfunsndc  6642  eqerlem  6701  qliftfuns  6756  eroveu  6763  cbvixp  6852  mptelixpg  6871  idssen  6918  pw2f1odclem  6983  xpf1o  6993  xpmapen  6999  findcard2d  7041  nnwetri  7066  fiintim  7081  snexxph  7105  fidcenumlemim  7107  fidcenumlemrk  7109  fidcenum  7111  supmoti  7148  isoti  7162  supisoti  7165  cnvti  7174  ordiso2  7190  ctssdccl  7266  finct  7271  infnninf  7279  nninfwlpoim  7334  nninfwlpo  7336  exmidontriimlem3  7393  exmidontriimlem4  7394  exmidontriim  7395  onntri13  7411  onntri51  7413  onntri3or  7418  dftap2  7425  netap  7428  2onetap  7429  2omotaplemap  7431  cc1  7439  cc2  7441  ltsopi  7495  addpipqqs  7545  mulpipqqs  7548  archpr  7818  cauappcvgprlemlol  7822  cauappcvgprlemopu  7823  cauappcvgprlemupu  7824  cauappcvgprlemdisj  7826  cauappcvgprlemladdru  7831  cauappcvgprlemladdrl  7832  cauappcvgprlemlim  7836  caucvgprlemlol  7845  caucvgprlemopu  7846  caucvgprlemupu  7847  caucvgprlemdisj  7849  caucvgprlemloc  7850  caucvgprlemcl  7851  caucvgprlemladdrl  7853  caucvgprprlemcbv  7862  caucvgprprlemopu  7874  caucvgprprlemclphr  7880  caucvgprprlemexbt  7881  suplocexprlemmu  7893  suplocexprlemdisj  7895  caucvgsrlembound  7969  caucvgsrlembnd  7976  suplocsrlem  7983  suplocsr  7984  peano1nnnn  8027  axcaucvglemres  8074  axpre-suploc  8077  negf1o  8516  lbreu  9080  lbinf  9083  suprubex  9086  suprlubex  9087  suprleubex  9089  1nn  9109  uzind4s  9773  uzind4s2  9774  indstr  9776  supinfneg  9778  infsupneg  9779  infregelbex  9781  eqreznegel  9797  lbzbi  9799  elpq  9832  zsupcl  10438  infssuzex  10440  infssuzledc  10441  zsupssdc  10445  exbtwnzlemex  10456  exbtwnz  10457  rebtwn2zlemstep  10459  rebtwn2z  10461  iseqovex  10667  iseqvalcbv  10668  seqvalcd  10670  seqovcd  10676  seq3f1olemqsum  10722  seq3f1olemp  10724  seq3f1oleml  10725  seqf1og  10730  seq3distr  10741  faclbnd6  10953  fimaxq  11036  wrd2ind  11241  reuccatpfxs1lem  11264  reuccatpfxs1  11265  cvg1nlemres  11482  resqrexlemsqa  11521  resqrexlemex  11522  cau3lem  11611  fclim  11791  climeu  11793  cn1lem  11811  climcau  11844  climcvg1n  11847  summodclem3  11877  summodclem2a  11878  summodclem2  11879  summodc  11880  zsumdc  11881  fsum3  11884  isumz  11886  isumss2  11890  fsumsersdc  11892  fsum3ser  11894  fsumadd  11903  fsum2dlemstep  11931  fisumcom2  11935  isumshft  11987  cvgratz  12029  mertensabs  12034  prodfdivap  12044  cbvprod  12055  prodmodclem3  12072  prodmodclem2a  12073  prodmodclem2  12074  prodmodc  12075  zproddc  12076  fprodseq  12080  fprodm1s  12098  fprodp1s  12099  fprod2dlemstep  12119  fprodcom2fi  12123  fprodsplitf  12129  odd2np1lem  12369  bitsfzolem  12451  bezoutlemmain  12505  bezoutlemeu  12514  gcdmultiple  12527  rplpwr  12534  nnwofdc  12545  nnwosdc  12546  nninfctlemfo  12547  isprm5lem  12649  isprm5  12650  pw2dvdseu  12676  hashdvds  12729  eulerthlemh  12739  reumodprminv  12762  pclemub  12796  pclemdc  12797  pceu  12804  pcmptdvds  12854  1arith  12876  4sqlem2  12898  4sqlem11  12910  4sqlem12  12911  ennnfonelemg  12960  ennnfoneleminc  12968  ennnfonelemkh  12969  ennnfonelemhf1o  12970  ennnfonelemex  12971  ennnfonelemhom  12972  ennnfonelemrnh  12973  ennnfonelemfun  12974  ennnfonelemdm  12977  ennnfonelemr  12980  ennnfone  12982  inffinp1  12986  ctinf  12987  nninfdclemf  13006  nninfdclemp1  13007  unbendc  13011  infpn2  13013  strsetsid  13051  mgmidmo  13391  lidrididd  13401  mndinvmod  13464  insubm  13504  dfgrp3mlem  13617  mulgaddcom  13669  mulginvcom  13670  isnsg2  13726  gsumfzconstf  13865  srgmulgass  13938  islmodd  14242  lmodvsmmulgdi  14272  rmodislmodlem  14299  rmodislmod  14300  lssats2  14363  mplsubgfilemcl  14648  baspartn  14709  cnpnei  14878  txdis1cn  14937  cnmptid  14940  xmetxp  15166  cncfmptc  15255  cncfmptid  15256  dedekindeulemloc  15278  dedekindicclemloc  15287  ivthinclemlr  15296  ivthinclemur  15298  ivthinclemloc  15300  ivthdec  15303  dvmptfsum  15384  plymullem1  15407  perfectlem2  15659  lgseisenlem2  15735  lgsquadlem3  15743  lgsquad  15744  lgsquad2lem2  15746  2lgslem1a  15752  usgruspgrben  15969  umgr2edg1  15992  umgr2edgneu  15995  usgredg4  15998  usgredgreu  15999  uspgredg2vtxeu  16001  spimd  16059  2spim  16060  ch2var  16061  bj-sbimedh  16065  bj-sbimeh  16066  cbvrald  16082  sumdc2  16093  bdth  16124  bdcdeq  16132  bdne  16146  bdreu  16148  bdcsn  16163  bdsep2  16179  bdsepnft  16180  bdsepnfALT  16182  bdbm1.3ii  16184  bj-nalset  16188  bj-zfpair2  16203  bj-bdfindes  16242  bj-nn0suc0  16243  bj-nntrans  16244  setindft  16258  setindis  16260  bdsetindis  16262  bj-inf2vnlem3  16265  bj-inf2vnlem4  16266  strcoll2  16276  strcollnft  16277  strcollnfALT  16279  sscoll2  16281  nnti  16287  2omap  16290  nnsf  16302  peano4nninf  16303  nninfsellemqall  16312  nninfomni  16316  nnnninfen  16318  trilpolemeq1  16339  tridceq  16355  redc0  16356  reap0  16357  dceqnconst  16359  dcapnconst  16360  nconstwlpolemgt0  16363