Theorem weq 1514

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

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

Syntax hints:   = wceq 1364

This theorem is referenced by:  alequcoms  1527  equidqe  1543  ax4sp1  1544  spimfv  1710  chvarfv  1711  equid  1712  nfequid  1713  stdpc6  1714  equcomi  1715  ax6evr  1716  equcom  1717  equcomd  1718  equcoms  1719  equtr  1720  equtrr  1721  equtr2  1722  equequ1  1723  equequ2  1724  ax11i  1725  ax10o  1726  ax10  1728  nfae  1730  hbaes  1731  hbnae  1732  nfnae  1733  hbnaes  1734  equsalh  1737  equsal  1738  dral1  1741  dral2  1742  drex2  1743  drnf1  1744  drnf2  1745  spimth  1746  spimh  1748  spimed  1751  cbv1  1756  cbv1h  1757  cbv1v  1758  cbv2h  1759  cbv2w  1761  cbvalv1  1762  cbvexv1  1763  cbvalh  1764  chvar  1768  sbimi  1775  sb1  1777  sb2  1778  sbequ1  1779  sbequ2  1780  sbequ12  1782  sbequ12r  1783  sbequ12a  1784  sbid  1785  stdpc4  1786  sbh  1787  sb6x  1790  sbequ5  1793  sbequ6  1794  equsb1  1796  equsb2  1797  sbiedh  1798  sbiedv  1800  sbieh  1801  equsalv  1804  equs5a  1805  drsb1  1810  exdistrfor  1811  sb4a  1812  equs45f  1813  sb6f  1814  sb5f  1815  sb4e  1816  hbsb2a  1817  hbsb2e  1818  sbcof2  1821  aev  1823  ax16  1824  dveeq2  1826  dveeq2or  1827  ax11v2  1831  ax11a2  1832  ax11b  1837  equs5  1840  equs5or  1841  sb3  1842  sb4  1843  sb4or  1844  sb4b  1845  sb4bor  1846  hbsb2  1847  nfsb2or  1848  sbequi  1850  sbequ  1851  drsb2  1852  spsbe  1853  spsbim  1854  sbequ8  1858  sbidm  1862  sb5rf  1863  sb6rf  1864  ax16i  1869  spv  1871  speiv  1873  equvin  1874  a16g  1875  a16gb  1876  a16nf  1877  sb56  1897  sb6  1898  sb5  1899  sbnv  1900  sbanv  1901  sborv  1902  sbi1v  1903  sbi2v  1904  cbvalvw  1931  cbvexvw  1932  cbval2  1933  cbvex2  1934  cbvaldva  1940  cbvexdva  1941  cbvex4v  1942  hbs1  1950  hbsbv  1953  nfsbxy  1954  nfsbxyt  1955  nfsbv  1959  equsb3  1963  sbco  1980  sbcocom  1982  sbcomxyyz  1984  sb9v  1990  2sb5  1995  2sb6  1996  sbcom2v  1997  sb6a  2000  2sb5rf  2001  2sb6rf  2002  dfsb7  2003  sb7f  2004  sb7af  2005  sb10f  2007  sbel2x  2010  sbalyz  2011  sbal1yz  2013  sbal1  2014  sbexyz  2015  exsb  2020  2exsb  2021  dvelimALT  2022  dvelimfv  2023  hbsb4t  2025  nfsb4t  2026  dvelimf  2027  dvelimdf  2028  dvelimor  2030  dveeq1  2031  sbal2  2032  euf  2043  eubidh  2044  eubid  2045  hbeu1  2048  nfeu1  2049  sb8eu  2051  nfeuv  2056  sb8euh  2061  eu1  2063  mo2n  2066  euex  2068  eumo0  2069  mo23  2079  mor  2080  modc  2081  eu2  2082  eu3h  2083  mo2r  2090  mo3h  2091  mo2dc  2093  mo4f  2098  eu4  2100  moim  2102  moimv  2104  moanim  2112  mopick  2116  2eu4  2131  euequ1  2133  exists1  2134  elequ1  2164  elequ2  2165  cleljust  2166  elsb1  2167  elsb2  2168  axext3  2172  axext4  2173  bm1.1  2174  eleq1w  2250  cleqh  2289  cbvabw  2312  cbvab  2313  sbab  2317  nfcjust  2320  drnfc1  2349  drnfc2  2350  nfabdw  2351  dvelimdc  2353  dvelimc  2354  nfcvf  2355  cbvralfw  2708  cbvrexfw  2709  cbvralf  2710  cbvrexf  2711  cbvreu  2716  cbvralvw  2722  cbvrexvw  2723  cbvreuvw  2724  cbvraldva2  2725  cbvrexdva2  2726  cbvraldva  2727  cbvrexdva  2728  cbvral2vw  2729  cbvrex2vw  2730  cbvral2v  2731  cbvrex2v  2732  cbvral3v  2733  sbralie  2736  cbvrab  2750  vjust  2753  vex  2755  rr19.3v  2891  rr19.28v  2892  ralab2  2916  rexab2  2918  reu2  2940  reu6  2941  reu3  2942  rmo4  2945  reu4  2946  reu7  2947  reu8  2948  rmo3f  2949  rmo4f  2950  cdeqi  2962  cdeqri  2963  cdeqth  2964  cdeqnot  2965  cdeqal  2966  cdeqab  2967  cdeqim  2970  cdeqcv  2971  cdeqeq  2972  cdeqel  2973  nfccdeq  2975  sbsbc  2981  sbc8g  2985  sbcco2  3000  sbc5  3001  sbcralt  3054  sbcralg  3056  sbcreug  3058  rmo3  3069  cbvcsbw  3076  cbvcsb  3077  csbcow  3083  sbcel12g  3087  sbceqg  3088  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  difjust  3145  unjust  3147  injust  3149  dfss2f  3161  dfdif3  3260  dfnul3  3440  dfif3  3562  preq12bg  3788  eluniab  3836  elintab  3870  int0  3873  dfiunv2  3937  cbviun  3938  cbviin  3939  cbvdisj  4005  disjiun  4013  sndisj  4014  sbcbrg  4072  cbvmptf  4112  cbvmpt  4113  axsep2  4137  bm1.3ii  4139  nalset  4148  zfpow  4193  el  4196  dtruarb  4209  copsexg  4262  opelopabsb  4278  swopo  4324  pofun  4330  issod  4337  frind  4370  zfun  4452  ruv  4567  dtru  4577  dcextest  4598  tfisi  4604  findes  4620  relop  4795  dfdmf  4838  dfrnf  4886  resiexg  4970  dfres2  4977  opabresid  4978  mptresid  4979  imai  5002  issref  5029  intasym  5031  cnvi  5051  rnxpid  5081  cnvpom  5189  nfiota1  5198  cbviota  5201  sb8iota  5203  iotaval  5207  iotanul  5211  iota4  5215  eliota  5223  eliotaeu  5224  csbiotag  5228  dffun2  5245  dffun4  5246  dffun5r  5247  dffun6f  5248  dffun4f  5251  sbcfung  5259  funopg  5269  funinsn  5284  funcnveq  5298  fun11  5302  fununi  5303  funcnvuni  5304  imain  5317  isarep2  5322  brprcneu  5527  fv2  5529  elfv  5532  fv3  5557  relelfvdm  5566  fvmpt2  5620  ralrnmpt  5679  rexrnmpt  5680  ffnfvf  5696  f1veqaeq  5791  dff13f  5792  fliftfuns  5820  canth  5850  cbvriota  5863  csbriotag  5865  acexmid  5896  oprabidlem  5928  cbvmpox  5975  cbvmpo  5976  cbvmpov  5977  mpofun  5999  abrexex2  6150  fmpoco  6242  f1o2ndf1  6254  poxp  6258  tposoprab  6306  tfrlem3-2d  6338  tfrlemi1  6358  tfr1onlemsucfn  6366  tfr1onlemaccex  6374  tfrcllemsucfn  6379  tfrcllemsucaccv  6380  tfrcllembxssdm  6382  tfrcllembfn  6383  tfrcllemaccex  6387  dcdifsnid  6530  fnsnsplitdc  6531  funresdfunsndc  6532  eqerlem  6591  qliftfuns  6646  eroveu  6653  cbvixp  6742  mptelixpg  6761  idssen  6804  pw2f1odclem  6863  xpf1o  6873  xpmapen  6879  findcard2d  6920  nnwetri  6945  fiintim  6958  snexxph  6980  fidcenumlemim  6982  fidcenumlemrk  6984  fidcenum  6986  supmoti  7023  isoti  7037  supisoti  7040  cnvti  7049  ordiso2  7065  ctssdccl  7141  finct  7146  infnninf  7153  nninfwlpoim  7207  nninfwlpo  7208  exmidontriimlem3  7253  exmidontriimlem4  7254  exmidontriim  7255  onntri13  7268  onntri51  7270  onntri3or  7275  dftap2  7281  netap  7284  2onetap  7285  2omotaplemap  7287  cc1  7295  cc2  7297  ltsopi  7350  addpipqqs  7400  mulpipqqs  7403  archpr  7673  cauappcvgprlemlol  7677  cauappcvgprlemopu  7678  cauappcvgprlemupu  7679  cauappcvgprlemdisj  7681  cauappcvgprlemladdru  7686  cauappcvgprlemladdrl  7687  cauappcvgprlemlim  7691  caucvgprlemlol  7700  caucvgprlemopu  7701  caucvgprlemupu  7702  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprlemcl  7706  caucvgprlemladdrl  7708  caucvgprprlemcbv  7717  caucvgprprlemopu  7729  caucvgprprlemclphr  7735  caucvgprprlemexbt  7736  suplocexprlemmu  7748  suplocexprlemdisj  7750  caucvgsrlembound  7824  caucvgsrlembnd  7831  suplocsrlem  7838  suplocsr  7839  peano1nnnn  7882  axcaucvglemres  7929  axpre-suploc  7932  negf1o  8370  lbreu  8933  lbinf  8936  suprubex  8939  suprlubex  8940  suprleubex  8942  1nn  8961  uzind4s  9622  uzind4s2  9623  indstr  9625  supinfneg  9627  infsupneg  9628  infregelbex  9630  eqreznegel  9646  lbzbi  9648  elpq  9680  exbtwnzlemex  10282  exbtwnz  10283  rebtwn2zlemstep  10285  rebtwn2z  10287  iseqovex  10489  iseqvalcbv  10490  seqvalcd  10492  seqovcd  10496  seq3f1olemqsum  10533  seq3f1olemp  10535  seq3f1oleml  10536  seq3distr  10547  faclbnd6  10759  fimaxq  10842  cvg1nlemres  11029  resqrexlemsqa  11068  resqrexlemex  11069  cau3lem  11158  fclim  11337  climeu  11339  cn1lem  11357  climcau  11390  climcvg1n  11393  summodclem3  11423  summodclem2a  11424  summodclem2  11425  summodc  11426  zsumdc  11427  fsum3  11430  isumz  11432  isumss2  11436  fsumsersdc  11438  fsum3ser  11440  fsumadd  11449  fsum2dlemstep  11477  fisumcom2  11481  isumshft  11533  cvgratz  11575  mertensabs  11580  prodfdivap  11590  cbvprod  11601  prodmodclem3  11618  prodmodclem2a  11619  prodmodclem2  11620  prodmodc  11621  zproddc  11622  fprodseq  11626  fprodm1s  11644  fprodp1s  11645  fprod2dlemstep  11665  fprodcom2fi  11669  fprodsplitf  11675  odd2np1lem  11912  zsupcl  11983  infssuzex  11985  infssuzledc  11986  zsupssdc  11990  bezoutlemmain  12034  bezoutlemeu  12043  gcdmultiple  12056  rplpwr  12063  nnwofdc  12074  nnwosdc  12075  isprm5lem  12176  isprm5  12177  pw2dvdseu  12203  hashdvds  12256  eulerthlemh  12266  reumodprminv  12288  pclemub  12322  pclemdc  12323  pceu  12330  pcmptdvds  12380  1arith  12402  4sqlem2  12424  4sqlem11  12436  4sqlem12  12437  ennnfonelemg  12457  ennnfoneleminc  12465  ennnfonelemkh  12466  ennnfonelemhf1o  12467  ennnfonelemex  12468  ennnfonelemhom  12469  ennnfonelemrnh  12470  ennnfonelemfun  12471  ennnfonelemdm  12474  ennnfonelemr  12477  ennnfone  12479  inffinp1  12483  ctinf  12484  nninfdclemf  12503  nninfdclemp1  12504  unbendc  12508  infpn2  12510  strsetsid  12548  mgmidmo  12851  lidrididd  12861  mndinvmod  12921  insubm  12952  dfgrp3mlem  13057  mulgaddcom  13103  mulginvcom  13104  isnsg2  13159  srgmulgass  13360  islmodd  13626  lmodvsmmulgdi  13656  rmodislmodlem  13683  rmodislmod  13684  lssats2  13747  baspartn  14027  cnpnei  14196  txdis1cn  14255  cnmptid  14258  xmetxp  14484  cncfmptc  14559  cncfmptid  14560  dedekindeulemloc  14574  dedekindicclemloc  14583  ivthinclemlr  14592  ivthinclemur  14594  ivthinclemloc  14596  ivthdec  14599  lgseisenlem2  14929  spimd  14995  2spim  14996  ch2var  14997  bj-sbimedh  15001  bj-sbimeh  15002  cbvrald  15018  sumdc2  15029  bdth  15061  bdcdeq  15069  bdne  15083  bdreu  15085  bdcsn  15100  bdsep2  15116  bdsepnft  15117  bdsepnfALT  15119  bdbm1.3ii  15121  bj-nalset  15125  bj-zfpair2  15140  bj-bdfindes  15179  bj-nn0suc0  15180  bj-nntrans  15181  setindft  15195  setindis  15197  bdsetindis  15199  bj-inf2vnlem3  15202  bj-inf2vnlem4  15203  strcoll2  15213  strcollnft  15214  strcollnfALT  15216  sscoll2  15218  nnti  15223  nnsf  15233  peano4nninf  15234  nninfsellemqall  15243  nninfomni  15247  trilpolemeq1  15267  tridceq  15283  redc0  15284  reap0  15285  dceqnconst  15287  dcapnconst  15288  nconstwlpolemgt0  15291