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 x = y

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1395	1 wff x = y

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  4259  el  4262  dtruarb  4275  copsexg  4330  opelopabsb  4348  swopo  4397  pofun  4403  issod  4410  frind  4443  zfun  4525  ruv  4642  dtru  4652  dcextest  4673  tfisi  4679  findes  4695  relop  4872  dfdmf  4916  dfrnf  4965  resiexg  5050  dfres2  5057  opabresid  5058  mptresid  5059  imai  5084  issref  5111  intasym  5113  cnvi  5133  rnxpid  5163  cnvpom  5271  nfiota1  5280  cbviota  5283  sb8iota  5286  iotaval  5290  iotanul  5294  iota4  5298  eliota  5306  eliotaeu  5307  csbiotag  5311  dffun2  5328  dffun4  5329  dffun5r  5330  dffun6f  5331  dffun4f  5334  sbcfung  5342  funopg  5352  fundif  5365  funinsn  5370  funcnveq  5384  fun11  5388  fununi  5389  funcnvuni  5390  imain  5403  isarep2  5408  brprcneu  5622  fv2  5624  elfv  5627  fv3  5652  relelfvdm  5661  fvmpt2  5720  ralrnmpt  5779  rexrnmpt  5780  ffnfvf  5796  f1veqaeq  5899  dff13f  5900  fliftfuns  5928  canth  5958  cbvriotavw  5971  cbvriota  5972  csbriotag  5974  acexmid  6006  oprabidlem  6038  cbvmpox  6088  cbvmpo  6089  cbvmpov  6090  mpofun  6112  abrexex2  6275  fmpoco  6368  f1o2ndf1  6380  poxp  6384  tposoprab  6432  tfrlem3-2d  6464  tfrlemi1  6484  tfr1onlemsucfn  6492  tfr1onlemaccex  6500  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  dcdifsnid  6658  fnsnsplitdc  6659  funresdfunsndc  6660  eqerlem  6719  qliftfuns  6774  eroveu  6781  cbvixp  6870  mptelixpg  6889  idssen  6936  pw2f1odclem  7003  xpf1o  7013  xpmapen  7019  findcard2d  7061  fidcen  7069  eqsndc  7076  nnwetri  7089  fiintim  7104  snexxph  7128  fidcenumlemim  7130  fidcenumlemrk  7132  fidcenum  7134  supmoti  7171  isoti  7185  supisoti  7188  cnvti  7197  ordiso2  7213  ctssdccl  7289  finct  7294  infnninf  7302  nninfwlpoim  7357  nninfwlpo  7359  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  onntri13  7434  onntri51  7436  onntri3or  7441  dftap2  7448  netap  7451  2onetap  7452  2omotaplemap  7454  cc1  7462  cc2  7464  ltsopi  7518  addpipqqs  7568  mulpipqqs  7571  archpr  7841  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlemlim  7859  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdrl  7876  caucvgprprlemcbv  7885  caucvgprprlemopu  7897  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  suplocexprlemmu  7916  suplocexprlemdisj  7918  caucvgsrlembound  7992  caucvgsrlembnd  7999  suplocsrlem  8006  suplocsr  8007  peano1nnnn  8050  axcaucvglemres  8097  axpre-suploc  8100  negf1o  8539  lbreu  9103  lbinf  9106  suprubex  9109  suprlubex  9110  suprleubex  9112  1nn  9132  uzind4s  9797  uzind4s2  9798  indstr  9800  supinfneg  9802  infsupneg  9803  infregelbex  9805  eqreznegel  9821  lbzbi  9823  elpq  9856  zsupcl  10463  infssuzex  10465  infssuzledc  10466  zsupssdc  10470  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2z  10486  iseqovex  10692  iseqvalcbv  10693  seqvalcd  10695  seqovcd  10701  seq3f1olemqsum  10747  seq3f1olemp  10749  seq3f1oleml  10750  seqf1og  10755  seq3distr  10766  faclbnd6  10978  fimaxq  11062  wrd2ind  11271  reuccatpfxs1lem  11294  reuccatpfxs1  11295  cvg1nlemres  11512  resqrexlemsqa  11551  resqrexlemex  11552  cau3lem  11641  fclim  11821  climeu  11823  cn1lem  11841  climcau  11874  climcvg1n  11877  summodclem3  11907  summodclem2a  11908  summodclem2  11909  summodc  11910  zsumdc  11911  fsum3  11914  isumz  11916  isumss2  11920  fsumsersdc  11922  fsum3ser  11924  fsumadd  11933  fsum2dlemstep  11961  fisumcom2  11965  isumshft  12017  cvgratz  12059  mertensabs  12064  prodfdivap  12074  cbvprod  12085  prodmodclem3  12102  prodmodclem2a  12103  prodmodclem2  12104  prodmodc  12105  zproddc  12106  fprodseq  12110  fprodm1s  12128  fprodp1s  12129  fprod2dlemstep  12149  fprodcom2fi  12153  fprodsplitf  12159  odd2np1lem  12399  bitsfzolem  12481  bezoutlemmain  12535  bezoutlemeu  12544  gcdmultiple  12557  rplpwr  12564  nnwofdc  12575  nnwosdc  12576  nninfctlemfo  12577  isprm5lem  12679  isprm5  12680  pw2dvdseu  12706  hashdvds  12759  eulerthlemh  12769  reumodprminv  12792  pclemub  12826  pclemdc  12827  pceu  12834  pcmptdvds  12884  1arith  12906  4sqlem2  12928  4sqlem11  12940  4sqlem12  12941  ennnfonelemg  12990  ennnfoneleminc  12998  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemrnh  13003  ennnfonelemfun  13004  ennnfonelemdm  13007  ennnfonelemr  13010  ennnfone  13012  inffinp1  13016  ctinf  13017  nninfdclemf  13036  nninfdclemp1  13037  unbendc  13041  infpn2  13043  strsetsid  13081  mgmidmo  13421  lidrididd  13431  mndinvmod  13494  insubm  13534  dfgrp3mlem  13647  mulgaddcom  13699  mulginvcom  13700  isnsg2  13756  gsumfzconstf  13895  srgmulgass  13968  islmodd  14273  lmodvsmmulgdi  14303  rmodislmodlem  14330  rmodislmod  14331  lssats2  14394  mplsubgfilemcl  14679  baspartn  14740  cnpnei  14909  txdis1cn  14968  cnmptid  14971  xmetxp  15197  cncfmptc  15286  cncfmptid  15287  dedekindeulemloc  15309  dedekindicclemloc  15318  ivthinclemlr  15327  ivthinclemur  15329  ivthinclemloc  15331  ivthdec  15334  dvmptfsum  15415  plymullem1  15438  perfectlem2  15690  lgseisenlem2  15766  lgsquadlem3  15774  lgsquad  15775  lgsquad2lem2  15777  2lgslem1a  15783  usgruspgrben  16000  umgr2edg1  16023  umgr2edgneu  16026  usgredg4  16029  usgredgreu  16030  uspgredg2vtxeu  16032  vtxedgfi  16049  vtxlpfi  16050  spimd  16212  2spim  16213  ch2var  16214  bj-sbimedh  16218  bj-sbimeh  16219  cbvrald  16235  sumdc2  16246  bdth  16277  bdcdeq  16285  bdne  16299  bdreu  16301  bdcsn  16316  bdsep2  16332  bdsepnft  16333  bdsepnfALT  16335  bdbm1.3ii  16337  bj-nalset  16341  bj-zfpair2  16356  bj-bdfindes  16395  bj-nn0suc0  16396  bj-nntrans  16397  setindft  16411  setindis  16413  bdsetindis  16415  bj-inf2vnlem3  16418  bj-inf2vnlem4  16419  strcoll2  16429  strcollnft  16430  strcollnfALT  16432  sscoll2  16434  nnti  16443  2omap  16446  nnsf  16459  peano4nninf  16460  nninfsellemqall  16469  nninfomni  16473  nnnninfen  16475  trilpolemeq1  16496  tridceq  16512  redc0  16513  reap0  16514  dceqnconst  16516  dcapnconst  16517  nconstwlpolemgt0  16520