Theorem weq 1480

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

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

Syntax hints:   = wceq 1332

This theorem is referenced by:  alequcoms  1497  equidqe  1513  ax4sp1  1514  equid  1678  nfequid  1679  stdpc6  1680  equcomi  1681  ax6evr  1682  equcom  1683  equcomd  1684  equcoms  1685  equtr  1686  equtrr  1687  equtr2  1688  equequ1  1689  equequ2  1690  elequ1  1691  elequ2  1692  ax11i  1693  ax10o  1694  ax10  1696  nfae  1698  hbaes  1699  hbnae  1700  nfnae  1701  hbnaes  1702  equsalh  1705  equsal  1706  dral1  1709  dral2  1710  drex2  1711  drnf1  1712  drnf2  1713  spimth  1714  spimh  1716  spimed  1719  cbv1  1723  cbv1h  1724  cbv2h  1725  cbvalh  1727  chvar  1731  sbimi  1738  sb1  1740  sb2  1741  sbequ1  1742  sbequ2  1743  sbequ12  1745  sbequ12r  1746  sbequ12a  1747  sbid  1748  stdpc4  1749  sbh  1750  sb6x  1753  sbequ5  1756  sbequ6  1757  equsb1  1759  equsb2  1760  sbiedh  1761  sbiedv  1763  sbieh  1764  equs5a  1767  drsb1  1772  exdistrfor  1773  sb4a  1774  equs45f  1775  sb6f  1776  sb5f  1777  sb4e  1778  hbsb2a  1779  hbsb2e  1780  sbcof2  1783  aev  1785  ax16  1786  dveeq2  1788  dveeq2or  1789  ax11v2  1793  ax11a2  1794  ax11b  1799  equs5  1802  equs5or  1803  sb3  1804  sb4  1805  sb4or  1806  sb4b  1807  sb4bor  1808  hbsb2  1809  nfsb2or  1810  sbequi  1812  sbequ  1813  drsb2  1814  spsbe  1815  spsbim  1816  sbequ8  1820  sbidm  1824  sb5rf  1825  sb6rf  1826  ax16i  1831  spv  1833  speiv  1835  equvin  1836  a16g  1837  a16gb  1838  a16nf  1839  sb56  1858  sb6  1859  sb5  1860  sbnv  1861  sbanv  1862  sborv  1863  sbi1v  1864  sbi2v  1865  cbval2  1894  cbvex2  1895  cbvaldva  1901  cbvexdva  1902  cbvex4v  1903  cleljust  1911  hbs1  1912  hbsbv  1915  nfsbxy  1916  nfsbxyt  1917  equsb3  1925  sbco  1942  sbcocom  1944  sbcomxyyz  1946  elsb3  1952  elsb4  1953  sb9v  1954  2sb5  1959  2sb6  1960  sbcom2v  1961  sb6a  1964  2sb5rf  1965  2sb6rf  1966  dfsb7  1967  sb7f  1968  sb7af  1969  sb10f  1971  sbel2x  1974  sbalyz  1975  sbal1yz  1977  sbal1  1978  sbexyz  1979  exsb  1984  2exsb  1985  dvelimALT  1986  dvelimfv  1987  hbsb4t  1989  nfsb4t  1990  dvelimf  1991  dvelimdf  1992  dvelimor  1994  dveeq1  1995  sbal2  1998  euf  2005  eubidh  2006  eubid  2007  hbeu1  2010  nfeu1  2011  sb8eu  2013  nfeuv  2018  sb8euh  2023  eu1  2025  mo2n  2028  euex  2030  eumo0  2031  mo23  2041  mor  2042  modc  2043  eu2  2044  eu3h  2045  mo2r  2052  mo3h  2053  mo2dc  2055  mo4f  2060  eu4  2062  moim  2064  moimv  2066  moanim  2074  mopick  2078  2eu4  2093  euequ1  2095  exists1  2096  axext3  2123  axext4  2124  bm1.1  2125  eleq1w  2201  cleqh  2240  cbvab  2264  sbab  2268  nfcjust  2270  drnfc1  2299  drnfc2  2300  dvelimdc  2302  dvelimc  2303  nfcvf  2304  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvraldva2  2664  cbvrexdva2  2665  cbvraldva  2666  cbvrexdva  2667  cbvral2v  2668  cbvrex2v  2669  cbvral3v  2670  sbralie  2673  cbvrab  2687  vjust  2690  vex  2692  rr19.3v  2827  rr19.28v  2828  ralab2  2852  rexab2  2854  reu2  2876  reu6  2877  reu3  2878  rmo4  2881  reu4  2882  reu7  2883  reu8  2884  rmo3f  2885  rmo4f  2886  cdeqi  2898  cdeqri  2899  cdeqth  2900  cdeqnot  2901  cdeqal  2902  cdeqab  2903  cdeqim  2906  cdeqcv  2907  cdeqeq  2908  cdeqel  2909  nfccdeq  2911  sbsbc  2917  sbc8g  2920  sbcco2  2935  sbc5  2936  sbcralt  2989  sbcralg  2991  sbcreug  2993  rmo3  3004  cbvcsbw  3011  cbvcsb  3012  sbcel12g  3022  sbceqg  3023  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  difjust  3077  unjust  3079  injust  3081  dfss2f  3093  dfdif3  3191  dfnul3  3371  dfif3  3492  preq12bg  3708  eluniab  3756  elintab  3790  int0  3793  dfiunv2  3857  cbviun  3858  cbviin  3859  cbvdisj  3924  disjiun  3932  sndisj  3933  sbcbrg  3990  cbvmptf  4030  cbvmpt  4031  axsep2  4055  bm1.3ii  4057  nalset  4066  zfpow  4107  el  4110  dtruarb  4123  copsexg  4174  opelopabsb  4190  swopo  4236  pofun  4242  issod  4249  frind  4282  zfun  4364  ruv  4473  dtru  4483  dcextest  4503  tfisi  4509  findes  4525  relop  4697  dfdmf  4740  dfrnf  4788  resiexg  4872  dfres2  4879  opabresid  4880  mptresid  4881  imai  4903  issref  4929  intasym  4931  cnvi  4951  rnxpid  4981  cnvpom  5089  nfiota1  5098  cbviota  5101  sb8iota  5103  iotaval  5107  iotanul  5111  iota4  5114  csbiotag  5124  dffun2  5141  dffun4  5142  dffun5r  5143  dffun6f  5144  dffun4f  5147  sbcfung  5155  funopg  5165  funinsn  5180  funcnveq  5194  fun11  5198  fununi  5199  funcnvuni  5200  imain  5213  isarep2  5218  brprcneu  5422  fv2  5424  elfv  5427  fv3  5452  relelfvdm  5461  fvmpt2  5512  ralrnmpt  5570  rexrnmpt  5571  ffnfvf  5587  f1veqaeq  5678  dff13f  5679  fliftfuns  5707  cbvriota  5748  csbriotag  5750  acexmid  5781  oprabidlem  5810  cbvmpox  5857  cbvmpo  5858  cbvmpov  5859  mpofun  5881  abrexex2  6030  fmpoco  6121  f1o2ndf1  6133  poxp  6137  tposoprab  6185  tfrlem3-2d  6217  tfrlemi1  6237  tfr1onlemsucfn  6245  tfr1onlemaccex  6253  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  dcdifsnid  6408  fnsnsplitdc  6409  funresdfunsndc  6410  eqerlem  6468  qliftfuns  6521  eroveu  6528  cbvixp  6617  mptelixpg  6636  idssen  6679  xpf1o  6746  xpmapen  6752  findcard2d  6793  nnwetri  6812  fiintim  6825  snexxph  6846  fidcenumlemim  6848  fidcenumlemrk  6850  fidcenum  6852  supmoti  6888  isoti  6902  supisoti  6905  cnvti  6914  ordiso2  6928  ctssdccl  7004  finct  7009  cc1  7097  cc2  7099  ltsopi  7152  addpipqqs  7202  mulpipqqs  7205  archpr  7475  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlemlim  7493  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdrl  7510  caucvgprprlemcbv  7519  caucvgprprlemopu  7531  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  suplocexprlemmu  7550  suplocexprlemdisj  7552  caucvgsrlembound  7626  caucvgsrlembnd  7633  suplocsrlem  7640  suplocsr  7641  peano1nnnn  7684  axcaucvglemres  7731  axpre-suploc  7734  negf1o  8168  lbreu  8727  lbinf  8730  suprubex  8733  suprlubex  8734  suprleubex  8736  1nn  8755  uzind4s  9412  uzind4s2  9413  indstr  9415  supinfneg  9417  infsupneg  9418  eqreznegel  9433  lbzbi  9435  elpq  9467  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2z  10063  iseqovex  10260  iseqvalcbv  10261  seqvalcd  10263  seqovcd  10267  seq3f1olemqsum  10304  seq3f1olemp  10306  seq3f1oleml  10307  seq3distr  10317  faclbnd6  10522  fimaxq  10605  cvg1nlemres  10789  resqrexlemsqa  10828  resqrexlemex  10829  cau3lem  10918  fclim  11095  climeu  11097  cn1lem  11115  climcau  11148  climcvg1n  11151  summodclem3  11181  summodclem2a  11182  summodclem2  11183  summodc  11184  zsumdc  11185  fsum3  11188  isumz  11190  isumss2  11194  fsumsersdc  11196  fsum3ser  11198  fsumadd  11207  fsum2dlemstep  11235  fisumcom2  11239  isumshft  11291  cvgratz  11333  mertensabs  11338  prodfdivap  11348  cbvprod  11359  prodmodclem3  11376  prodmodclem2a  11377  prodmodclem2  11378  prodmodc  11379  zproddc  11380  fprodseq  11384  odd2np1lem  11605  zsupcl  11676  infssuzex  11678  infssuzledc  11679  bezoutlemmain  11722  bezoutlemeu  11731  gcdmultiple  11744  rplpwr  11751  pw2dvdseu  11882  hashdvds  11933  ennnfonelemg  11952  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemrnh  11965  ennnfonelemfun  11966  ennnfonelemdm  11969  ennnfonelemr  11972  ennnfone  11974  inffinp1  11978  ctinf  11979  strsetsid  12031  baspartn  12256  cnpnei  12427  txdis1cn  12486  cnmptid  12489  xmetxp  12715  cncfmptc  12790  cncfmptid  12791  dedekindeulemloc  12805  dedekindicclemloc  12814  ivthinclemlr  12823  ivthinclemur  12825  ivthinclemloc  12827  ivthdec  12830  spimd  13143  2spim  13144  ch2var  13145  bj-sbimedh  13149  bj-sbimeh  13150  cbvrald  13166  sumdc2  13177  bdth  13200  bdcdeq  13208  bdne  13222  bdreu  13224  bdcsn  13239  bdsep2  13255  bdsepnft  13256  bdsepnfALT  13258  bdbm1.3ii  13260  bj-nalset  13264  bj-zfpair2  13279  bj-bdfindes  13318  bj-nn0suc0  13319  bj-nntrans  13320  setindft  13334  setindis  13336  bdsetindis  13338  bj-inf2vnlem3  13341  bj-inf2vnlem4  13342  strcoll2  13352  strcollnft  13353  strcollnfALT  13355  sscoll2  13357  nnti  13362  nnsf  13374  peano4nninf  13375  nninfsellemqall  13386  nninfomni  13390  trilpolemeq1  13408  dceqnconst  13423