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  3851  eluniab  3900  elintab  3934  int0  3937  dfiunv2  4001  cbviun  4002  cbviin  4003  cbvdisj  4069  invdisjrab  4077  disjiun  4078  sndisj  4079  sbcbrg  4138  cbvmptf  4178  cbvmpt  4179  axsep2  4203  bm1.3ii  4205  nalset  4214  zfpow  4260  el  4263  dtruarb  4276  copsexg  4331  opelopabsb  4349  swopo  4398  pofun  4404  issod  4411  frind  4444  zfun  4526  ruv  4643  dtru  4653  dcextest  4674  tfisi  4680  findes  4696  relop  4875  dfdmf  4919  dfrnf  4968  resiexg  5053  dfres2  5060  opabresid  5061  mptresid  5062  imai  5087  issref  5114  intasym  5116  cnvi  5136  rnxpid  5166  cnvpom  5274  nfiota1  5283  cbviota  5286  sb8iota  5289  iotaval  5293  iotanul  5297  iota4  5301  eliota  5309  eliotaeu  5310  csbiotag  5314  dffun2  5331  dffun4  5332  dffun5r  5333  dffun6f  5334  dffun4f  5337  sbcfung  5345  funopg  5355  fundif  5368  funinsn  5373  funcnveq  5387  fun11  5391  fununi  5392  funcnvuni  5393  imain  5406  isarep2  5411  brprcneu  5625  fv2  5627  elfv  5630  fv3  5655  relelfvdm  5664  fvmpt2  5723  ralrnmpt  5782  rexrnmpt  5783  ffnfvf  5799  f1veqaeq  5902  dff13f  5903  fliftfuns  5931  canth  5961  cbvriotavw  5974  cbvriota  5975  csbriotag  5977  acexmid  6009  oprabidlem  6041  cbvmpox  6091  cbvmpo  6092  cbvmpov  6093  mpofun  6115  abrexex2  6278  fmpoco  6373  f1o2ndf1  6385  poxp  6389  tposoprab  6437  tfrlem3-2d  6469  tfrlemi1  6489  tfr1onlemsucfn  6497  tfr1onlemaccex  6505  tfrcllemsucfn  6510  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemaccex  6518  dcdifsnid  6663  fnsnsplitdc  6664  funresdfunsndc  6665  eqerlem  6724  qliftfuns  6779  eroveu  6786  cbvixp  6875  mptelixpg  6894  idssen  6941  pw2f1odclem  7008  xpf1o  7018  xpmapen  7024  findcard2d  7066  fidcen  7074  eqsndc  7081  nnwetri  7094  fiintim  7109  snexxph  7133  fidcenumlemim  7135  fidcenumlemrk  7137  fidcenum  7139  supmoti  7176  isoti  7190  supisoti  7193  cnvti  7202  ordiso2  7218  ctssdccl  7294  finct  7299  infnninf  7307  nninfwlpoim  7362  nninfwlpo  7364  exmidontriimlem3  7421  exmidontriimlem4  7422  exmidontriim  7423  onntri13  7439  onntri51  7441  onntri3or  7446  dftap2  7453  netap  7456  2onetap  7457  2omotaplemap  7459  cc1  7467  cc2  7469  ltsopi  7523  addpipqqs  7573  mulpipqqs  7576  archpr  7846  cauappcvgprlemlol  7850  cauappcvgprlemopu  7851  cauappcvgprlemupu  7852  cauappcvgprlemdisj  7854  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  cauappcvgprlemlim  7864  caucvgprlemlol  7873  caucvgprlemopu  7874  caucvgprlemupu  7875  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlemcl  7879  caucvgprlemladdrl  7881  caucvgprprlemcbv  7890  caucvgprprlemopu  7902  caucvgprprlemclphr  7908  caucvgprprlemexbt  7909  suplocexprlemmu  7921  suplocexprlemdisj  7923  caucvgsrlembound  7997  caucvgsrlembnd  8004  suplocsrlem  8011  suplocsr  8012  peano1nnnn  8055  axcaucvglemres  8102  axpre-suploc  8105  negf1o  8544  lbreu  9108  lbinf  9111  suprubex  9114  suprlubex  9115  suprleubex  9117  1nn  9137  uzind4s  9802  uzind4s2  9803  indstr  9805  supinfneg  9807  infsupneg  9808  infregelbex  9810  eqreznegel  9826  lbzbi  9828  elpq  9861  zsupcl  10468  infssuzex  10470  infssuzledc  10471  zsupssdc  10475  exbtwnzlemex  10486  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2z  10491  iseqovex  10697  iseqvalcbv  10698  seqvalcd  10700  seqovcd  10706  seq3f1olemqsum  10752  seq3f1olemp  10754  seq3f1oleml  10755  seqf1og  10760  seq3distr  10771  faclbnd6  10983  fimaxq  11067  wrd2ind  11276  reuccatpfxs1lem  11299  reuccatpfxs1  11300  cvg1nlemres  11517  resqrexlemsqa  11556  resqrexlemex  11557  cau3lem  11646  fclim  11826  climeu  11828  cn1lem  11846  climcau  11879  climcvg1n  11882  summodclem3  11912  summodclem2a  11913  summodclem2  11914  summodc  11915  zsumdc  11916  fsum3  11919  isumz  11921  isumss2  11925  fsumsersdc  11927  fsum3ser  11929  fsumadd  11938  fsum2dlemstep  11966  fisumcom2  11970  isumshft  12022  cvgratz  12064  mertensabs  12069  prodfdivap  12079  cbvprod  12090  prodmodclem3  12107  prodmodclem2a  12108  prodmodclem2  12109  prodmodc  12110  zproddc  12111  fprodseq  12115  fprodm1s  12133  fprodp1s  12134  fprod2dlemstep  12154  fprodcom2fi  12158  fprodsplitf  12164  odd2np1lem  12404  bitsfzolem  12486  bezoutlemmain  12540  bezoutlemeu  12549  gcdmultiple  12562  rplpwr  12569  nnwofdc  12580  nnwosdc  12581  nninfctlemfo  12582  isprm5lem  12684  isprm5  12685  pw2dvdseu  12711  hashdvds  12764  eulerthlemh  12774  reumodprminv  12797  pclemub  12831  pclemdc  12832  pceu  12839  pcmptdvds  12889  1arith  12911  4sqlem2  12933  4sqlem11  12945  4sqlem12  12946  ennnfonelemg  12995  ennnfoneleminc  13003  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemex  13006  ennnfonelemhom  13007  ennnfonelemrnh  13008  ennnfonelemfun  13009  ennnfonelemdm  13012  ennnfonelemr  13015  ennnfone  13017  inffinp1  13021  ctinf  13022  nninfdclemf  13041  nninfdclemp1  13042  unbendc  13046  infpn2  13048  strsetsid  13086  mgmidmo  13426  lidrididd  13436  mndinvmod  13499  insubm  13539  dfgrp3mlem  13652  mulgaddcom  13704  mulginvcom  13705  isnsg2  13761  gsumfzconstf  13900  srgmulgass  13973  islmodd  14278  lmodvsmmulgdi  14308  rmodislmodlem  14335  rmodislmod  14336  lssats2  14399  mplsubgfilemcl  14684  baspartn  14745  cnpnei  14914  txdis1cn  14973  cnmptid  14976  xmetxp  15202  cncfmptc  15291  cncfmptid  15292  dedekindeulemloc  15314  dedekindicclemloc  15323  ivthinclemlr  15332  ivthinclemur  15334  ivthinclemloc  15336  ivthdec  15339  dvmptfsum  15420  plymullem1  15443  perfectlem2  15695  lgseisenlem2  15771  lgsquadlem3  15779  lgsquad  15780  lgsquad2lem2  15782  2lgslem1a  15788  usgruspgrben  16005  umgr2edg1  16028  umgr2edgneu  16031  usgredg4  16034  usgredgreu  16035  uspgredg2vtxeu  16037  vtxedgfi  16075  vtxlpfi  16076  spimd  16238  2spim  16239  ch2var  16240  bj-sbimedh  16244  bj-sbimeh  16245  cbvrald  16261  sumdc2  16272  bdth  16303  bdcdeq  16311  bdne  16325  bdreu  16327  bdcsn  16342  bdsep2  16358  bdsepnft  16359  bdsepnfALT  16361  bdbm1.3ii  16363  bj-nalset  16367  bj-zfpair2  16382  bj-bdfindes  16421  bj-nn0suc0  16422  bj-nntrans  16423  setindft  16437  setindis  16439  bdsetindis  16441  bj-inf2vnlem3  16444  bj-inf2vnlem4  16445  strcoll2  16455  strcollnft  16456  strcollnfALT  16458  sscoll2  16460  nnti  16469  2omap  16472  nnsf  16485  peano4nninf  16486  nninfsellemqall  16495  nninfomni  16499  nnnninfen  16501  trilpolemeq1  16522  tridceq  16538  redc0  16539  reap0  16540  dceqnconst  16542  dcapnconst  16543  nconstwlpolemgt0  16546