Theorem weq 1491

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

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

Syntax hints:   = wceq 1343

This theorem is referenced by:  alequcoms  1504  equidqe  1520  ax4sp1  1521  spimfv  1687  chvarfv  1688  equid  1689  nfequid  1690  stdpc6  1691  equcomi  1692  ax6evr  1693  equcom  1694  equcomd  1695  equcoms  1696  equtr  1697  equtrr  1698  equtr2  1699  equequ1  1700  equequ2  1701  ax11i  1702  ax10o  1703  ax10  1705  nfae  1707  hbaes  1708  hbnae  1709  nfnae  1710  hbnaes  1711  equsalh  1714  equsal  1715  dral1  1718  dral2  1719  drex2  1720  drnf1  1721  drnf2  1722  spimth  1723  spimh  1725  spimed  1728  cbv1  1733  cbv1h  1734  cbv1v  1735  cbv2h  1736  cbv2w  1738  cbvalv1  1739  cbvexv1  1740  cbvalh  1741  chvar  1745  sbimi  1752  sb1  1754  sb2  1755  sbequ1  1756  sbequ2  1757  sbequ12  1759  sbequ12r  1760  sbequ12a  1761  sbid  1762  stdpc4  1763  sbh  1764  sb6x  1767  sbequ5  1770  sbequ6  1771  equsb1  1773  equsb2  1774  sbiedh  1775  sbiedv  1777  sbieh  1778  equsalv  1781  equs5a  1782  drsb1  1787  exdistrfor  1788  sb4a  1789  equs45f  1790  sb6f  1791  sb5f  1792  sb4e  1793  hbsb2a  1794  hbsb2e  1795  sbcof2  1798  aev  1800  ax16  1801  dveeq2  1803  dveeq2or  1804  ax11v2  1808  ax11a2  1809  ax11b  1814  equs5  1817  equs5or  1818  sb3  1819  sb4  1820  sb4or  1821  sb4b  1822  sb4bor  1823  hbsb2  1824  nfsb2or  1825  sbequi  1827  sbequ  1828  drsb2  1829  spsbe  1830  spsbim  1831  sbequ8  1835  sbidm  1839  sb5rf  1840  sb6rf  1841  ax16i  1846  spv  1848  speiv  1850  equvin  1851  a16g  1852  a16gb  1853  a16nf  1854  sb56  1873  sb6  1874  sb5  1875  sbnv  1876  sbanv  1877  sborv  1878  sbi1v  1879  sbi2v  1880  cbvalvw  1907  cbvexvw  1908  cbval2  1909  cbvex2  1910  cbvaldva  1916  cbvexdva  1917  cbvex4v  1918  hbs1  1926  hbsbv  1929  nfsbxy  1930  nfsbxyt  1931  nfsbv  1935  equsb3  1939  sbco  1956  sbcocom  1958  sbcomxyyz  1960  sb9v  1966  2sb5  1971  2sb6  1972  sbcom2v  1973  sb6a  1976  2sb5rf  1977  2sb6rf  1978  dfsb7  1979  sb7f  1980  sb7af  1981  sb10f  1983  sbel2x  1986  sbalyz  1987  sbal1yz  1989  sbal1  1990  sbexyz  1991  exsb  1996  2exsb  1997  dvelimALT  1998  dvelimfv  1999  hbsb4t  2001  nfsb4t  2002  dvelimf  2003  dvelimdf  2004  dvelimor  2006  dveeq1  2007  sbal2  2008  euf  2019  eubidh  2020  eubid  2021  hbeu1  2024  nfeu1  2025  sb8eu  2027  nfeuv  2032  sb8euh  2037  eu1  2039  mo2n  2042  euex  2044  eumo0  2045  mo23  2055  mor  2056  modc  2057  eu2  2058  eu3h  2059  mo2r  2066  mo3h  2067  mo2dc  2069  mo4f  2074  eu4  2076  moim  2078  moimv  2080  moanim  2088  mopick  2092  2eu4  2107  euequ1  2109  exists1  2110  elequ1  2140  elequ2  2141  cleljust  2142  elsb1  2143  elsb2  2144  axext3  2148  axext4  2149  bm1.1  2150  eleq1w  2227  cleqh  2266  cbvabw  2289  cbvab  2290  sbab  2294  nfcjust  2296  drnfc1  2325  drnfc2  2326  nfabdw  2327  dvelimdc  2329  dvelimc  2330  nfcvf  2331  cbvralfw  2683  cbvrexfw  2684  cbvralf  2685  cbvrexf  2686  cbvreu  2690  cbvralvw  2696  cbvrexvw  2697  cbvreuvw  2698  cbvraldva2  2699  cbvrexdva2  2700  cbvraldva  2701  cbvrexdva  2702  cbvral2vw  2703  cbvrex2vw  2704  cbvral2v  2705  cbvrex2v  2706  cbvral3v  2707  sbralie  2710  cbvrab  2724  vjust  2727  vex  2729  rr19.3v  2865  rr19.28v  2866  ralab2  2890  rexab2  2892  reu2  2914  reu6  2915  reu3  2916  rmo4  2919  reu4  2920  reu7  2921  reu8  2922  rmo3f  2923  rmo4f  2924  cdeqi  2936  cdeqri  2937  cdeqth  2938  cdeqnot  2939  cdeqal  2940  cdeqab  2941  cdeqim  2944  cdeqcv  2945  cdeqeq  2946  cdeqel  2947  nfccdeq  2949  sbsbc  2955  sbc8g  2958  sbcco2  2973  sbc5  2974  sbcralt  3027  sbcralg  3029  sbcreug  3031  rmo3  3042  cbvcsbw  3049  cbvcsb  3050  csbcow  3056  sbcel12g  3060  sbceqg  3061  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  difjust  3117  unjust  3119  injust  3121  dfss2f  3133  dfdif3  3232  dfnul3  3412  dfif3  3533  preq12bg  3753  eluniab  3801  elintab  3835  int0  3838  dfiunv2  3902  cbviun  3903  cbviin  3904  cbvdisj  3969  disjiun  3977  sndisj  3978  sbcbrg  4036  cbvmptf  4076  cbvmpt  4077  axsep2  4101  bm1.3ii  4103  nalset  4112  zfpow  4154  el  4157  dtruarb  4170  copsexg  4222  opelopabsb  4238  swopo  4284  pofun  4290  issod  4297  frind  4330  zfun  4412  ruv  4527  dtru  4537  dcextest  4558  tfisi  4564  findes  4580  relop  4754  dfdmf  4797  dfrnf  4845  resiexg  4929  dfres2  4936  opabresid  4937  mptresid  4938  imai  4960  issref  4986  intasym  4988  cnvi  5008  rnxpid  5038  cnvpom  5146  nfiota1  5155  cbviota  5158  sb8iota  5160  iotaval  5164  iotanul  5168  iota4  5171  csbiotag  5181  dffun2  5198  dffun4  5199  dffun5r  5200  dffun6f  5201  dffun4f  5204  sbcfung  5212  funopg  5222  funinsn  5237  funcnveq  5251  fun11  5255  fununi  5256  funcnvuni  5257  imain  5270  isarep2  5275  brprcneu  5479  fv2  5481  elfv  5484  fv3  5509  relelfvdm  5518  fvmpt2  5569  ralrnmpt  5627  rexrnmpt  5628  ffnfvf  5644  f1veqaeq  5737  dff13f  5738  fliftfuns  5766  canth  5796  cbvriota  5808  csbriotag  5810  acexmid  5841  oprabidlem  5873  cbvmpox  5920  cbvmpo  5921  cbvmpov  5922  mpofun  5944  abrexex2  6092  fmpoco  6184  f1o2ndf1  6196  poxp  6200  tposoprab  6248  tfrlem3-2d  6280  tfrlemi1  6300  tfr1onlemsucfn  6308  tfr1onlemaccex  6316  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemaccex  6329  dcdifsnid  6472  fnsnsplitdc  6473  funresdfunsndc  6474  eqerlem  6532  qliftfuns  6585  eroveu  6592  cbvixp  6681  mptelixpg  6700  idssen  6743  xpf1o  6810  xpmapen  6816  findcard2d  6857  nnwetri  6881  fiintim  6894  snexxph  6915  fidcenumlemim  6917  fidcenumlemrk  6919  fidcenum  6921  supmoti  6958  isoti  6972  supisoti  6975  cnvti  6984  ordiso2  7000  ctssdccl  7076  finct  7081  infnninf  7088  exmidontriimlem3  7179  exmidontriimlem4  7180  exmidontriim  7181  onntri13  7194  onntri51  7196  onntri3or  7201  cc1  7206  cc2  7208  ltsopi  7261  addpipqqs  7311  mulpipqqs  7314  archpr  7584  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemupu  7590  cauappcvgprlemdisj  7592  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlemlim  7602  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemupu  7613  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemcl  7617  caucvgprlemladdrl  7619  caucvgprprlemcbv  7628  caucvgprprlemopu  7640  caucvgprprlemclphr  7646  caucvgprprlemexbt  7647  suplocexprlemmu  7659  suplocexprlemdisj  7661  caucvgsrlembound  7735  caucvgsrlembnd  7742  suplocsrlem  7749  suplocsr  7750  peano1nnnn  7793  axcaucvglemres  7840  axpre-suploc  7843  negf1o  8280  lbreu  8840  lbinf  8843  suprubex  8846  suprlubex  8847  suprleubex  8849  1nn  8868  uzind4s  9528  uzind4s2  9529  indstr  9531  supinfneg  9533  infsupneg  9534  infregelbex  9536  eqreznegel  9552  lbzbi  9554  elpq  9586  exbtwnzlemex  10185  exbtwnz  10186  rebtwn2zlemstep  10188  rebtwn2z  10190  iseqovex  10391  iseqvalcbv  10392  seqvalcd  10394  seqovcd  10398  seq3f1olemqsum  10435  seq3f1olemp  10437  seq3f1oleml  10438  seq3distr  10448  faclbnd6  10657  fimaxq  10740  cvg1nlemres  10927  resqrexlemsqa  10966  resqrexlemex  10967  cau3lem  11056  fclim  11235  climeu  11237  cn1lem  11255  climcau  11288  climcvg1n  11291  summodclem3  11321  summodclem2a  11322  summodclem2  11323  summodc  11324  zsumdc  11325  fsum3  11328  isumz  11330  isumss2  11334  fsumsersdc  11336  fsum3ser  11338  fsumadd  11347  fsum2dlemstep  11375  fisumcom2  11379  isumshft  11431  cvgratz  11473  mertensabs  11478  prodfdivap  11488  cbvprod  11499  prodmodclem3  11516  prodmodclem2a  11517  prodmodclem2  11518  prodmodc  11519  zproddc  11520  fprodseq  11524  fprodm1s  11542  fprodp1s  11543  fprod2dlemstep  11563  fprodcom2fi  11567  fprodsplitf  11573  odd2np1lem  11809  zsupcl  11880  infssuzex  11882  infssuzledc  11883  zsupssdc  11887  bezoutlemmain  11931  bezoutlemeu  11940  gcdmultiple  11953  rplpwr  11960  nnwofdc  11971  nnwosdc  11972  isprm5lem  12073  isprm5  12074  pw2dvdseu  12100  hashdvds  12153  eulerthlemh  12163  reumodprminv  12185  pclemub  12219  pclemdc  12220  pceu  12227  pcmptdvds  12275  1arith  12297  4sqlem2  12319  ennnfonelemg  12336  ennnfoneleminc  12344  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemrnh  12349  ennnfonelemfun  12350  ennnfonelemdm  12353  ennnfonelemr  12356  ennnfone  12358  inffinp1  12362  ctinf  12363  nninfdclemf  12382  nninfdclemp1  12383  unbendc  12387  infpn2  12389  strsetsid  12427  mgmidmo  12603  lidrididd  12613  baspartn  12688  cnpnei  12859  txdis1cn  12918  cnmptid  12921  xmetxp  13147  cncfmptc  13222  cncfmptid  13223  dedekindeulemloc  13237  dedekindicclemloc  13246  ivthinclemlr  13255  ivthinclemur  13257  ivthinclemloc  13259  ivthdec  13262  spimd  13646  2spim  13647  ch2var  13648  bj-sbimedh  13652  bj-sbimeh  13653  cbvrald  13669  sumdc2  13680  bdth  13713  bdcdeq  13721  bdne  13735  bdreu  13737  bdcsn  13752  bdsep2  13768  bdsepnft  13769  bdsepnfALT  13771  bdbm1.3ii  13773  bj-nalset  13777  bj-zfpair2  13792  bj-bdfindes  13831  bj-nn0suc0  13832  bj-nntrans  13833  setindft  13847  setindis  13849  bdsetindis  13851  bj-inf2vnlem3  13854  bj-inf2vnlem4  13855  strcoll2  13865  strcollnft  13866  strcollnfALT  13868  sscoll2  13870  nnti  13874  nnsf  13885  peano4nninf  13886  nninfsellemqall  13895  nninfomni  13899  trilpolemeq1  13919  tridceq  13935  redc0  13936  reap0  13937  dceqnconst  13938  dcapnconst  13939  nconstwlpolemgt0  13942