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  2798  vjust  2801  vex  2803  rr19.3v  2943  rr19.28v  2944  ralab2  2968  rexab2  2970  reu2  2992  reu6  2993  reu3  2994  rmo4  2997  reu4  2998  reu7  2999  reu8  3000  rmo3f  3001  rmo4f  3002  cdeqi  3014  cdeqri  3015  cdeqth  3016  cdeqnot  3017  cdeqal  3018  cdeqab  3019  cdeqim  3022  cdeqcv  3023  cdeqeq  3024  cdeqel  3025  nfccdeq  3027  sbsbc  3033  sbc8g  3037  sbcco2  3052  sbc5  3053  sbcralt  3106  sbcralg  3108  sbcreug  3110  reu8nf  3111  rmo3  3122  cbvcsbw  3129  cbvcsb  3130  csbcow  3136  sbcel12g  3140  sbceqg  3141  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  difjust  3199  unjust  3201  injust  3203  dfss2f  3216  dfdif3  3315  dfnul3  3495  dfif3  3617  rabsnifsb  3735  preq12bg  3854  eluniab  3903  elintab  3937  int0  3940  dfiunv2  4004  cbviun  4005  cbviin  4006  cbvdisj  4072  invdisjrab  4080  disjiun  4081  sndisj  4082  sbcbrg  4141  cbvmptf  4181  cbvmpt  4182  axsep2  4206  bm1.3ii  4208  nalset  4217  zfpow  4263  el  4266  dtruarb  4279  copsexg  4334  opelopabsb  4352  swopo  4401  pofun  4407  issod  4414  frind  4447  zfun  4529  ruv  4646  dtru  4656  dcextest  4677  tfisi  4683  findes  4699  relop  4878  dfdmf  4922  dfrnf  4971  resiexg  5056  dfres2  5063  opabresid  5064  mptresid  5065  imai  5090  issref  5117  intasym  5119  cnvi  5139  rnxpid  5169  cnvpom  5277  nfiota1  5286  cbviota  5289  sb8iota  5292  iotaval  5296  iotanul  5300  iota4  5304  eliota  5312  eliotaeu  5313  csbiotag  5317  dffun2  5334  dffun4  5335  dffun5r  5336  dffun6f  5337  dffun4f  5340  sbcfung  5348  funopg  5358  fundif  5371  funinsn  5376  funcnveq  5390  fun11  5394  fununi  5395  funcnvuni  5396  imain  5409  isarep2  5414  brprcneu  5628  fv2  5630  elfv  5633  fv3  5658  relelfvdm  5667  fvmpt2  5726  ralrnmpt  5785  rexrnmpt  5786  ffnfvf  5802  f1veqaeq  5905  dff13f  5906  fliftfuns  5934  canth  5964  cbvriotavw  5977  cbvriota  5978  csbriotag  5980  acexmid  6012  oprabidlem  6044  cbvmpox  6094  cbvmpo  6095  cbvmpov  6096  mpofun  6118  abrexex2  6281  fmpoco  6376  f1o2ndf1  6388  poxp  6392  tposoprab  6441  tfrlem3-2d  6473  tfrlemi1  6493  tfr1onlemsucfn  6501  tfr1onlemaccex  6509  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  dcdifsnid  6667  fnsnsplitdc  6668  funresdfunsndc  6669  eqerlem  6728  qliftfuns  6783  eroveu  6790  cbvixp  6879  mptelixpg  6898  idssen  6945  modom  6989  pw2f1odclem  7015  xpf1o  7025  xpmapen  7031  findcard2d  7075  fidcen  7083  eqsndc  7090  nnwetri  7103  fiintim  7118  snexxph  7143  fidcenumlemim  7145  fidcenumlemrk  7147  fidcenum  7149  supmoti  7186  isoti  7200  supisoti  7203  cnvti  7212  ordiso2  7228  ctssdccl  7304  finct  7309  infnninf  7317  nninfwlpoim  7372  nninfwlpo  7374  exmidontriimlem3  7431  exmidontriimlem4  7432  exmidontriim  7433  onntri13  7449  onntri51  7451  onntri3or  7456  dftap2  7463  netap  7466  2onetap  7467  2omotaplemap  7469  cc1  7477  cc2  7479  ltsopi  7533  addpipqqs  7583  mulpipqqs  7586  archpr  7856  cauappcvgprlemlol  7860  cauappcvgprlemopu  7861  cauappcvgprlemupu  7862  cauappcvgprlemdisj  7864  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  cauappcvgprlemlim  7874  caucvgprlemlol  7883  caucvgprlemopu  7884  caucvgprlemupu  7885  caucvgprlemdisj  7887  caucvgprlemloc  7888  caucvgprlemcl  7889  caucvgprlemladdrl  7891  caucvgprprlemcbv  7900  caucvgprprlemopu  7912  caucvgprprlemclphr  7918  caucvgprprlemexbt  7919  suplocexprlemmu  7931  suplocexprlemdisj  7933  caucvgsrlembound  8007  caucvgsrlembnd  8014  suplocsrlem  8021  suplocsr  8022  peano1nnnn  8065  axcaucvglemres  8112  axpre-suploc  8115  negf1o  8554  lbreu  9118  lbinf  9121  suprubex  9124  suprlubex  9125  suprleubex  9127  1nn  9147  uzind4s  9817  uzind4s2  9818  indstr  9820  supinfneg  9822  infsupneg  9823  infregelbex  9825  eqreznegel  9841  lbzbi  9843  elpq  9876  zsupcl  10484  infssuzex  10486  infssuzledc  10487  zsupssdc  10491  exbtwnzlemex  10502  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2z  10507  iseqovex  10713  iseqvalcbv  10714  seqvalcd  10716  seqovcd  10722  seq3f1olemqsum  10768  seq3f1olemp  10770  seq3f1oleml  10771  seqf1og  10776  seq3distr  10787  faclbnd6  10999  fimaxq  11084  wrd2ind  11297  reuccatpfxs1lem  11320  reuccatpfxs1  11321  cvg1nlemres  11539  resqrexlemsqa  11578  resqrexlemex  11579  cau3lem  11668  fclim  11848  climeu  11850  cn1lem  11868  climcau  11901  climcvg1n  11904  summodclem3  11934  summodclem2a  11935  summodclem2  11936  summodc  11937  zsumdc  11938  fsum3  11941  isumz  11943  isumss2  11947  fsumsersdc  11949  fsum3ser  11951  fsumadd  11960  fsum2dlemstep  11988  fisumcom2  11992  isumshft  12044  cvgratz  12086  mertensabs  12091  prodfdivap  12101  cbvprod  12112  prodmodclem3  12129  prodmodclem2a  12130  prodmodclem2  12131  prodmodc  12132  zproddc  12133  fprodseq  12137  fprodm1s  12155  fprodp1s  12156  fprod2dlemstep  12176  fprodcom2fi  12180  fprodsplitf  12186  odd2np1lem  12426  bitsfzolem  12508  bezoutlemmain  12562  bezoutlemeu  12571  gcdmultiple  12584  rplpwr  12591  nnwofdc  12602  nnwosdc  12603  nninfctlemfo  12604  isprm5lem  12706  isprm5  12707  pw2dvdseu  12733  hashdvds  12786  eulerthlemh  12796  reumodprminv  12819  pclemub  12853  pclemdc  12854  pceu  12861  pcmptdvds  12911  1arith  12933  4sqlem2  12955  4sqlem11  12967  4sqlem12  12968  ennnfonelemg  13017  ennnfoneleminc  13025  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemex  13028  ennnfonelemhom  13029  ennnfonelemrnh  13030  ennnfonelemfun  13031  ennnfonelemdm  13034  ennnfonelemr  13037  ennnfone  13039  inffinp1  13043  ctinf  13044  nninfdclemf  13063  nninfdclemp1  13064  unbendc  13068  infpn2  13070  strsetsid  13108  mgmidmo  13448  lidrididd  13458  mndinvmod  13521  insubm  13561  dfgrp3mlem  13674  mulgaddcom  13726  mulginvcom  13727  isnsg2  13783  gsumfzconstf  13922  srgmulgass  13995  islmodd  14300  lmodvsmmulgdi  14330  rmodislmodlem  14357  rmodislmod  14358  lssats2  14421  mplsubgfilemcl  14706  baspartn  14767  cnpnei  14936  txdis1cn  14995  cnmptid  14998  xmetxp  15224  cncfmptc  15313  cncfmptid  15314  dedekindeulemloc  15336  dedekindicclemloc  15345  ivthinclemlr  15354  ivthinclemur  15356  ivthinclemloc  15358  ivthdec  15361  dvmptfsum  15442  plymullem1  15465  perfectlem2  15717  lgseisenlem2  15793  lgsquadlem3  15801  lgsquad  15802  lgsquad2lem2  15804  2lgslem1a  15810  usgruspgrben  16030  umgr2edg1  16053  umgr2edgneu  16056  usgredg4  16059  usgredgreu  16060  uspgredg2vtxeu  16062  vtxedgfi  16100  vtxlpfi  16101  spimd  16311  2spim  16312  ch2var  16313  bj-sbimedh  16317  bj-sbimeh  16318  cbvrald  16334  sumdc2  16345  bdth  16376  bdcdeq  16384  bdne  16398  bdreu  16400  bdcsn  16415  bdsep2  16431  bdsepnft  16432  bdsepnfALT  16434  bdbm1.3ii  16436  bj-nalset  16440  bj-zfpair2  16455  bj-bdfindes  16494  bj-nn0suc0  16495  bj-nntrans  16496  setindft  16510  setindis  16512  bdsetindis  16514  bj-inf2vnlem3  16517  bj-inf2vnlem4  16518  strcoll2  16528  strcollnft  16529  strcollnfALT  16531  sscoll2  16533  nnti  16541  2omap  16544  nnsf  16557  peano4nninf  16558  nninfsellemqall  16567  nninfomni  16571  nnnninfen  16573  trilpolemeq1  16594  tridceq  16610  redc0  16611  reap0  16612  dceqnconst  16614  dcapnconst  16615  nconstwlpolemgt0  16618