Theorem weq 1552

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

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

Syntax hints:   = wceq 1398

This theorem is referenced by:  alequcoms  1565  equidqe  1581  ax4sp1  1582  spimfv  1747  chvarfv  1748  equid  1749  nfequid  1750  stdpc6  1751  equcomi  1752  ax6evr  1753  equcom  1754  equcomd  1755  equcoms  1756  equtr  1757  equtrr  1758  equtr2  1759  equequ1  1760  equequ2  1761  ax11i  1762  ax10o  1763  ax10  1765  nfae  1767  hbaes  1768  hbnae  1769  nfnae  1770  hbnaes  1771  equsalh  1774  equsal  1775  dral1  1778  dral2  1779  drex2  1780  drnf1  1781  drnf2  1782  spimth  1783  spimh  1785  spimed  1788  cbv1  1793  cbv1h  1794  cbv1v  1795  cbv2h  1796  cbv2w  1798  cbvalv1  1799  cbvexv1  1800  cbvalh  1801  chvar  1805  sbimi  1812  sb1  1814  sb2  1815  sbequ1  1816  sbequ2  1817  sbequ12  1819  sbequ12r  1820  sbequ12a  1821  sbid  1822  stdpc4  1823  sbh  1824  sb6x  1827  sbequ5  1830  sbequ6  1831  equsb1  1833  equsb2  1834  sbiedh  1835  sbiedv  1837  sbieh  1838  equsalv  1841  equs5a  1842  drsb1  1847  exdistrfor  1848  sb4a  1849  equs45f  1850  sb6f  1851  sb5f  1852  sb4e  1853  hbsb2a  1854  hbsb2e  1855  sbcof2  1858  aev  1860  ax16  1861  dveeq2  1863  dveeq2or  1864  ax11v2  1868  ax11a2  1869  ax11b  1874  equs5  1877  equs5or  1878  sb3  1879  sb4  1880  sb4or  1881  sb4b  1882  sb4bor  1883  hbsb2  1884  nfsb2or  1885  sbequi  1887  sbequ  1888  drsb2  1889  spsbe  1890  spsbim  1891  sbequ8  1895  sbidm  1899  sb5rf  1900  sb6rf  1901  ax16i  1906  spv  1908  speiv  1910  equvin  1911  a16g  1912  a16gb  1913  a16nf  1914  sb56  1934  sb6  1935  sb5  1936  sbnv  1937  sbanv  1938  sborv  1939  sbi1v  1940  sbi2v  1941  cbvalvw  1968  cbvexvw  1969  cbval2  1970  cbvex2  1971  cbvaldva  1977  cbvexdva  1978  cbvaldvaw  1979  cbval2vw  1981  cbvex2vw  1982  cbvex4v  1983  hbs1  1991  hbsbv  1994  nfsbxy  1995  nfsbxyt  1996  nfsbv  2000  equsb3  2004  sbco  2021  sbcocom  2023  sbcomxyyz  2025  sb9v  2031  2sb5  2036  2sb6  2037  sbcom2v  2038  sb6a  2041  2sb5rf  2042  2sb6rf  2043  dfsb7  2044  sb7f  2045  sb7af  2046  sb10f  2048  sbel2x  2051  sbalyz  2052  sbal1yz  2054  sbal1  2055  sbexyz  2056  exsb  2061  2exsb  2062  dvelimALT  2063  dvelimfv  2064  hbsb4t  2066  nfsb4t  2067  dvelimf  2068  dvelimdf  2069  dvelimor  2071  dveeq1  2072  sbal2  2073  euf  2084  eubidh  2085  eubid  2086  hbeu1  2089  nfeu1  2090  sb8eu  2092  nfeuv  2097  sb8euh  2102  eu1  2104  mo2n  2107  euex  2109  eumo0  2110  mo23  2121  mor  2122  modc  2123  eu2  2124  eu3h  2125  mo2r  2132  mo3h  2133  mo2dc  2135  mo4f  2140  eu4  2142  moim  2144  moimv  2146  moanim  2154  mopick  2158  2eu4  2173  euequ1  2175  exists1  2176  elequ1  2206  elequ2  2207  cleljust  2208  elsb1  2209  elsb2  2210  axext3  2214  axext4  2215  bm1.1  2216  eleq1w  2292  cleqh  2331  abbib  2349  cbvabw  2355  cbvab  2356  sbab  2360  nfcjust  2363  drnfc1  2392  drnfc2  2393  nfabdw  2394  dvelimdc  2396  dvelimc  2397  nfcvf  2398  cbvrmow  2717  cbvralfw  2757  cbvrexfw  2758  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvralvw  2772  cbvrexvw  2773  cbvreuvw  2774  cbvraldva2  2775  cbvrexdva2  2776  cbvraldva  2777  cbvrexdva  2778  cbvral2vw  2779  cbvrex2vw  2780  cbvral2v  2781  cbvrex2v  2782  cbvral3v  2783  sbralie  2786  cbvrab  2801  vjust  2804  vex  2806  rr19.3v  2946  rr19.28v  2947  ralab2  2971  rexab2  2973  reu2  2995  reu6  2996  reu3  2997  rmo4  3000  reu4  3001  reu7  3002  reu8  3003  rmo3f  3004  rmo4f  3005  cdeqi  3017  cdeqri  3018  cdeqth  3019  cdeqnot  3020  cdeqal  3021  cdeqab  3022  cdeqim  3025  cdeqcv  3026  cdeqeq  3027  cdeqel  3028  nfccdeq  3030  sbsbc  3036  sbc8g  3040  sbcco2  3055  sbc5  3056  sbcralt  3109  sbcralg  3111  sbcreug  3113  reu8nf  3114  rmo3  3125  cbvcsbw  3132  cbvcsb  3133  csbcow  3139  sbcel12g  3143  sbceqg  3144  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  difjust  3202  unjust  3204  injust  3206  dfss2f  3219  dfdif3  3319  dfnul3  3499  dfif3  3623  rabsnifsb  3741  preq12bg  3861  eluniab  3910  elintab  3944  int0  3947  dfiunv2  4011  cbviun  4012  cbviin  4013  cbvdisj  4079  invdisjrab  4087  disjiun  4088  sndisj  4089  sbcbrg  4148  cbvmptf  4188  cbvmpt  4189  axsep2  4213  bm1.3ii  4215  nalset  4224  zfpow  4271  el  4274  dtruarb  4287  copsexg  4342  opelopabsb  4360  swopo  4409  pofun  4415  issod  4422  frind  4455  zfun  4537  ruv  4654  dtru  4664  dcextest  4685  tfisi  4691  findes  4707  relop  4886  dfdmf  4930  dfrnf  4979  resiexg  5064  dfres2  5071  opabresid  5072  mptresid  5073  imai  5099  issref  5126  intasym  5128  cnvi  5148  rnxpid  5178  cnvpom  5286  nfiota1  5295  cbviota  5298  sb8iota  5301  iotaval  5305  iotanul  5309  iota4  5313  eliota  5321  eliotaeu  5322  csbiotag  5326  dffun2  5343  dffun4  5344  dffun5r  5345  dffun6f  5346  dffun4f  5349  sbcfung  5357  funopg  5367  fundif  5381  funinsn  5386  funcnveq  5400  fun11  5404  fununi  5405  funcnvuni  5406  imain  5419  isarep2  5424  brprcneu  5641  fv2  5643  elfv  5646  fv3  5671  relelfvdm  5680  fvmpt2  5739  ralrnmpt  5797  rexrnmpt  5798  ffnfvf  5814  f1veqaeq  5920  dff13f  5921  fliftfuns  5949  canth  5979  cbvriotavw  5992  cbvriota  5993  csbriotag  5995  acexmid  6027  oprabidlem  6059  cbvmpox  6109  cbvmpo  6110  cbvmpov  6111  mpofun  6133  abrexex2  6295  fmpoco  6390  f1o2ndf1  6402  poxp  6406  suppfnss  6435  tposoprab  6489  tfrlem3-2d  6521  tfrlemi1  6541  tfr1onlemsucfn  6549  tfr1onlemaccex  6557  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  dcdifsnid  6715  fnsnsplitdc  6716  funresdfunsndc  6717  eqerlem  6776  qliftfuns  6831  eroveu  6838  cbvixp  6927  mptelixpg  6946  idssen  6993  modom  7037  pw2f1odclem  7063  xpf1o  7073  xpmapen  7079  findcard2d  7123  fidcen  7131  eqsndc  7138  nnwetri  7151  fiintim  7166  snexxph  7192  fidcenumlemim  7194  fidcenumlemrk  7196  fidcenum  7198  supmoti  7252  isoti  7266  supisoti  7269  cnvti  7278  ordiso2  7294  ctssdccl  7370  finct  7375  infnninf  7383  nninfwlpoim  7438  nninfwlpo  7440  sspw1or2  7463  exmidontriimlem3  7498  exmidontriimlem4  7499  exmidontriim  7500  onntri13  7516  onntri51  7518  onntri3or  7523  dftap2  7530  netap  7533  2onetap  7534  2omotaplemap  7536  cc1  7544  cc2  7546  ltsopi  7600  addpipqqs  7650  mulpipqqs  7653  archpr  7923  cauappcvgprlemlol  7927  cauappcvgprlemopu  7928  cauappcvgprlemupu  7929  cauappcvgprlemdisj  7931  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlemlim  7941  caucvgprlemlol  7950  caucvgprlemopu  7951  caucvgprlemupu  7952  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemcl  7956  caucvgprlemladdrl  7958  caucvgprprlemcbv  7967  caucvgprprlemopu  7979  caucvgprprlemclphr  7985  caucvgprprlemexbt  7986  suplocexprlemmu  7998  suplocexprlemdisj  8000  caucvgsrlembound  8074  caucvgsrlembnd  8081  suplocsrlem  8088  suplocsr  8089  peano1nnnn  8132  axcaucvglemres  8179  axpre-suploc  8182  negf1o  8620  lbreu  9184  lbinf  9187  suprubex  9190  suprlubex  9191  suprleubex  9193  1nn  9213  uzind4s  9885  uzind4s2  9886  indstr  9888  supinfneg  9890  infsupneg  9891  infregelbex  9893  eqreznegel  9909  lbzbi  9911  elpq  9944  zsupcl  10554  infssuzex  10556  infssuzledc  10557  zsupssdc  10561  exbtwnzlemex  10572  exbtwnz  10573  rebtwn2zlemstep  10575  rebtwn2z  10577  iseqovex  10783  iseqvalcbv  10784  seqvalcd  10786  seqovcd  10792  seq3f1olemqsum  10838  seq3f1olemp  10840  seq3f1oleml  10841  seqf1og  10846  seq3distr  10857  faclbnd6  11069  fimaxq  11154  wrd2ind  11370  reuccatpfxs1lem  11393  reuccatpfxs1  11394  cvg1nlemres  11625  resqrexlemsqa  11664  resqrexlemex  11665  cau3lem  11754  fclim  11934  climeu  11936  cn1lem  11954  climcau  11987  climcvg1n  11990  summodclem3  12021  summodclem2a  12022  summodclem2  12023  summodc  12024  zsumdc  12025  fsum3  12028  isumz  12030  isumss2  12034  fsumsersdc  12036  fsum3ser  12038  fsumadd  12047  fsum2dlemstep  12075  fisumcom2  12079  isumshft  12131  cvgratz  12173  mertensabs  12178  prodfdivap  12188  cbvprod  12199  prodmodclem3  12216  prodmodclem2a  12217  prodmodclem2  12218  prodmodc  12219  zproddc  12220  fprodseq  12224  fprodm1s  12242  fprodp1s  12243  fprod2dlemstep  12263  fprodcom2fi  12267  fprodsplitf  12273  odd2np1lem  12513  bitsfzolem  12595  bezoutlemmain  12649  bezoutlemeu  12658  gcdmultiple  12671  rplpwr  12678  nnwofdc  12689  nnwosdc  12690  nninfctlemfo  12691  isprm5lem  12793  isprm5  12794  pw2dvdseu  12820  hashdvds  12873  eulerthlemh  12883  reumodprminv  12906  pclemub  12940  pclemdc  12941  pceu  12948  pcmptdvds  12998  1arith  13020  4sqlem2  13042  4sqlem11  13054  4sqlem12  13055  ennnfonelemg  13104  ennnfoneleminc  13112  ennnfonelemkh  13113  ennnfonelemhf1o  13114  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemrnh  13117  ennnfonelemfun  13118  ennnfonelemdm  13121  ennnfonelemr  13124  ennnfone  13126  inffinp1  13130  ctinf  13131  nninfdclemf  13150  nninfdclemp1  13151  unbendc  13155  infpn2  13157  strsetsid  13195  mgmidmo  13535  lidrididd  13545  mndinvmod  13608  insubm  13648  dfgrp3mlem  13761  mulgaddcom  13813  mulginvcom  13814  isnsg2  13870  gsumfzconstf  14009  srgmulgass  14083  islmodd  14389  lmodvsmmulgdi  14419  rmodislmodlem  14446  rmodislmod  14447  lssats2  14510  mplsubgfilemcl  14800  baspartn  14861  cnpnei  15030  txdis1cn  15089  cnmptid  15092  xmetxp  15318  cncfmptc  15407  cncfmptid  15408  dedekindeulemloc  15430  dedekindicclemloc  15439  ivthinclemlr  15448  ivthinclemur  15450  ivthinclemloc  15452  ivthdec  15455  dvmptfsum  15536  plymullem1  15559  perfectlem2  15814  lgseisenlem2  15890  lgsquadlem3  15898  lgsquad  15899  lgsquad2lem2  15901  2lgslem1a  15907  usgruspgrben  16127  umgr2edg1  16150  umgr2edgneu  16153  usgredg4  16156  usgredgreu  16157  uspgredg2vtxeu  16159  vtxedgfi  16230  vtxlpfi  16231  depindlem1  16447  depindlem2  16448  depindlem3  16449  spimd  16483  2spim  16484  ch2var  16485  bj-sbimedh  16489  bj-sbimeh  16490  cbvrald  16506  sumdc2  16517  bdth  16547  bdcdeq  16555  bdne  16569  bdreu  16571  bdcsn  16586  bdsep2  16602  bdsepnft  16603  bdsepnfALT  16605  bdbm1.3ii  16607  bj-nalset  16611  bj-zfpair2  16626  bj-bdfindes  16665  bj-nn0suc0  16666  bj-nntrans  16667  setindft  16681  setindis  16683  bdsetindis  16685  bj-inf2vnlem3  16688  bj-inf2vnlem4  16689  strcoll2  16699  strcollnft  16700  strcollnfALT  16702  sscoll2  16704  nnti  16712  2omap  16715  nnsf  16731  peano4nninf  16732  nninfsellemqall  16741  nninfomni  16745  nnnninfen  16747  repiecef  16760  trilpolemeq1  16772  tridceq  16789  redc0  16790  reap0  16791  dceqnconst  16793  dcapnconst  16794  nconstwlpolemgt0  16797