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 𝑥 = 𝑦

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1398	1 wff 𝑥 = 𝑦

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  7235  isoti  7249  supisoti  7252  cnvti  7261  ordiso2  7277  ctssdccl  7353  finct  7358  infnninf  7366  nninfwlpoim  7421  nninfwlpo  7423  sspw1or2  7446  exmidontriimlem3  7481  exmidontriimlem4  7482  exmidontriim  7483  onntri13  7499  onntri51  7501  onntri3or  7506  dftap2  7513  netap  7516  2onetap  7517  2omotaplemap  7519  cc1  7527  cc2  7529  ltsopi  7583  addpipqqs  7633  mulpipqqs  7636  archpr  7906  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlemlim  7924  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdrl  7941  caucvgprprlemcbv  7950  caucvgprprlemopu  7962  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  suplocexprlemmu  7981  suplocexprlemdisj  7983  caucvgsrlembound  8057  caucvgsrlembnd  8064  suplocsrlem  8071  suplocsr  8072  peano1nnnn  8115  axcaucvglemres  8162  axpre-suploc  8165  negf1o  8604  lbreu  9168  lbinf  9171  suprubex  9174  suprlubex  9175  suprleubex  9177  1nn  9197  uzind4s  9867  uzind4s2  9868  indstr  9870  supinfneg  9872  infsupneg  9873  infregelbex  9875  eqreznegel  9891  lbzbi  9893  elpq  9926  zsupcl  10535  infssuzex  10537  infssuzledc  10538  zsupssdc  10542  exbtwnzlemex  10553  exbtwnz  10554  rebtwn2zlemstep  10556  rebtwn2z  10558  iseqovex  10764  iseqvalcbv  10765  seqvalcd  10767  seqovcd  10773  seq3f1olemqsum  10819  seq3f1olemp  10821  seq3f1oleml  10822  seqf1og  10827  seq3distr  10838  faclbnd6  11050  fimaxq  11135  wrd2ind  11351  reuccatpfxs1lem  11374  reuccatpfxs1  11375  cvg1nlemres  11606  resqrexlemsqa  11645  resqrexlemex  11646  cau3lem  11735  fclim  11915  climeu  11917  cn1lem  11935  climcau  11968  climcvg1n  11971  summodclem3  12002  summodclem2a  12003  summodclem2  12004  summodc  12005  zsumdc  12006  fsum3  12009  isumz  12011  isumss2  12015  fsumsersdc  12017  fsum3ser  12019  fsumadd  12028  fsum2dlemstep  12056  fisumcom2  12060  isumshft  12112  cvgratz  12154  mertensabs  12159  prodfdivap  12169  cbvprod  12180  prodmodclem3  12197  prodmodclem2a  12198  prodmodclem2  12199  prodmodc  12200  zproddc  12201  fprodseq  12205  fprodm1s  12223  fprodp1s  12224  fprod2dlemstep  12244  fprodcom2fi  12248  fprodsplitf  12254  odd2np1lem  12494  bitsfzolem  12576  bezoutlemmain  12630  bezoutlemeu  12639  gcdmultiple  12652  rplpwr  12659  nnwofdc  12670  nnwosdc  12671  nninfctlemfo  12672  isprm5lem  12774  isprm5  12775  pw2dvdseu  12801  hashdvds  12854  eulerthlemh  12864  reumodprminv  12887  pclemub  12921  pclemdc  12922  pceu  12929  pcmptdvds  12979  1arith  13001  4sqlem2  13023  4sqlem11  13035  4sqlem12  13036  ennnfonelemg  13085  ennnfoneleminc  13093  ennnfonelemkh  13094  ennnfonelemhf1o  13095  ennnfonelemex  13096  ennnfonelemhom  13097  ennnfonelemrnh  13098  ennnfonelemfun  13099  ennnfonelemdm  13102  ennnfonelemr  13105  ennnfone  13107  inffinp1  13111  ctinf  13112  nninfdclemf  13131  nninfdclemp1  13132  unbendc  13136  infpn2  13138  strsetsid  13176  mgmidmo  13516  lidrididd  13526  mndinvmod  13589  insubm  13629  dfgrp3mlem  13742  mulgaddcom  13794  mulginvcom  13795  isnsg2  13851  gsumfzconstf  13990  srgmulgass  14064  islmodd  14369  lmodvsmmulgdi  14399  rmodislmodlem  14426  rmodislmod  14427  lssats2  14490  mplsubgfilemcl  14780  baspartn  14841  cnpnei  15010  txdis1cn  15069  cnmptid  15072  xmetxp  15298  cncfmptc  15387  cncfmptid  15388  dedekindeulemloc  15410  dedekindicclemloc  15419  ivthinclemlr  15428  ivthinclemur  15430  ivthinclemloc  15432  ivthdec  15435  dvmptfsum  15516  plymullem1  15539  perfectlem2  15794  lgseisenlem2  15870  lgsquadlem3  15878  lgsquad  15879  lgsquad2lem2  15881  2lgslem1a  15887  usgruspgrben  16107  umgr2edg1  16130  umgr2edgneu  16133  usgredg4  16136  usgredgreu  16137  uspgredg2vtxeu  16139  vtxedgfi  16210  vtxlpfi  16211  depindlem1  16427  depindlem2  16428  depindlem3  16429  spimd  16463  2spim  16464  ch2var  16465  bj-sbimedh  16469  bj-sbimeh  16470  cbvrald  16486  sumdc2  16497  bdth  16527  bdcdeq  16535  bdne  16549  bdreu  16551  bdcsn  16566  bdsep2  16582  bdsepnft  16583  bdsepnfALT  16585  bdbm1.3ii  16587  bj-nalset  16591  bj-zfpair2  16606  bj-bdfindes  16645  bj-nn0suc0  16646  bj-nntrans  16647  setindft  16661  setindis  16663  bdsetindis  16665  bj-inf2vnlem3  16668  bj-inf2vnlem4  16669  strcoll2  16679  strcollnft  16680  strcollnfALT  16682  sscoll2  16684  nnti  16692  2omap  16695  nnsf  16711  peano4nninf  16712  nninfsellemqall  16721  nninfomni  16725  nnnninfen  16727  repiecef  16740  trilpolemeq1  16752  tridceq  16769  redc0  16770  reap0  16771  dceqnconst  16773  dcapnconst  16774  nconstwlpolemgt0  16777