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  1779  dral2  1780  drex2  1781  drnf1  1782  drnf2  1783  spimth  1784  spimh  1786  spimed  1789  cbv1  1794  cbv1h  1795  cbv1v  1796  cbv2h  1797  cbv2w  1799  cbvalv1  1800  cbvexv1  1801  cbvalh  1802  chvar  1806  sbimi  1813  sb1  1815  sb2  1816  sbequ1  1817  sbequ2  1818  sbequ12  1820  sbequ12r  1821  sbequ12a  1822  sbid  1823  stdpc4  1824  sbh  1825  sb6x  1828  sbequ5  1831  sbequ6  1832  equsb1  1834  equsb2  1835  sbiedh  1836  sbiedv  1838  sbieh  1839  equsalv  1842  equs5a  1843  drsb1  1848  exdistrfor  1849  sb4a  1850  equs45f  1851  sb6f  1852  sb5f  1853  sb4e  1854  hbsb2a  1855  hbsb2e  1856  sbcof2  1859  aev  1861  ax16  1862  dveeq2  1864  dveeq2or  1865  ax11v2  1869  ax11a2  1870  ax11b  1875  equs5  1878  equs5or  1879  sb3  1880  sb4  1881  sb4or  1882  sb4b  1883  sb4bor  1884  hbsb2  1885  nfsb2or  1886  sbequi  1888  sbequ  1889  drsb2  1890  spsbe  1891  spsbim  1892  sbequ8  1896  sbidm  1900  sb5rf  1901  sb6rf  1902  ax16i  1907  spv  1909  speiv  1911  equvin  1912  a16g  1913  a16gb  1914  a16nf  1915  sb56  1935  sb6  1936  sb5  1937  sbnv  1938  sbanv  1939  sborv  1940  sbi1v  1941  sbi2v  1942  cbvalvw  1969  cbvexvw  1970  cbval2  1971  cbvex2  1972  cbvaldva  1978  cbvexdva  1979  cbvaldvaw  1980  cbval2vw  1982  cbvex2vw  1983  cbvex4v  1984  hbs1  1992  hbsbv  1995  nfsbxy  1996  nfsbxyt  1997  nfsbv  2001  equsb3  2005  sbco  2022  sbcocom  2024  sbcomxyyz  2026  sb9v  2032  2sb5  2037  2sb6  2038  sbcom2v  2039  sb6a  2042  2sb5rf  2043  2sb6rf  2044  dfsb7  2045  sb7f  2046  sb7af  2047  sb10f  2049  sbel2x  2052  sbalyz  2053  sbal1yz  2055  sbal1  2056  sbexyz  2057  exsb  2062  2exsb  2063  dvelimALT  2064  dvelimfv  2065  hbsb4t  2067  nfsb4t  2068  dvelimf  2069  dvelimdf  2070  dvelimor  2072  dveeq1  2073  sbal2  2074  euf  2085  eubidh  2086  eubid  2087  hbeu1  2090  nfeu1  2091  sb8eu  2093  nfeuv  2098  sb8euh  2103  eu1  2105  mo2n  2108  euex  2110  eumo0  2111  mo23  2122  mor  2123  modc  2124  eu2  2125  eu3h  2126  mo2r  2133  mo3h  2134  mo2dc  2136  mo4f  2141  eu4  2143  moim  2145  moimv  2147  moanim  2155  mopick  2159  2eu4  2174  euequ1  2176  exists1  2177  elequ1  2207  elequ2  2208  cleljust  2209  elsb1  2210  elsb2  2211  axext3  2215  axext4  2216  bm1.1  2217  eleq1w  2293  cleqh  2332  abbib  2350  cbvabw  2357  cbvab  2358  sbab  2362  nfcjust  2372  drnfc1  2401  drnfc2  2402  nfabdw  2403  dvelimdc  2405  dvelimc  2406  nfcvf  2407  cbvrmow  2726  cbvralfw  2766  cbvrexfw  2767  cbvralf  2768  cbvrexf  2769  cbvreu  2775  cbvralvw  2781  cbvrexvw  2782  cbvreuvw  2783  cbvraldva2  2784  cbvrexdva2  2785  cbvraldva  2786  cbvrexdva  2787  cbvral2vw  2788  cbvrex2vw  2789  cbvral2v  2790  cbvrex2v  2791  cbvral3v  2792  sbralie  2795  cbvrab  2810  vjust  2813  vex  2815  rr19.3v  2955  rr19.28v  2956  ralab2  2980  rexab2  2982  reu2  3004  reu6  3005  reu3  3006  rmo4  3009  reu4  3010  reu7  3011  reu8  3012  rmo3f  3013  rmo4f  3014  cdeqi  3026  cdeqri  3027  cdeqth  3028  cdeqnot  3029  cdeqal  3030  cdeqab  3031  cdeqim  3034  cdeqcv  3035  cdeqeq  3036  cdeqel  3037  nfccdeq  3039  sbsbc  3045  sbc8g  3049  sbcco2  3064  sbc5  3065  sbcralt  3118  sbcralg  3120  sbcreug  3122  reu8nf  3123  rmo3  3134  cbvcsbw  3141  cbvcsb  3142  csbcow  3148  sbcel12g  3152  sbceqg  3153  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  difjust  3211  unjust  3213  injust  3215  dfss2f  3228  dfdif3  3328  dfnul3  3510  dfif3  3635  rabsnifsb  3756  preq12bg  3876  eluniab  3925  elintab  3959  int0  3962  dfiunv2  4026  cbviun  4027  cbviin  4028  cbvdisj  4094  invdisjrab  4102  disjiun  4103  sndisj  4104  sbcbrg  4163  cbvmptf  4203  cbvmpt  4204  axsep2  4228  bm1.3ii  4230  nalset  4239  zfpow  4287  el  4290  dtruarb  4303  copsexg  4359  opelopabsb  4377  swopo  4426  pofun  4432  issod  4439  frind  4472  zfun  4554  ruv  4671  dtru  4681  dcextest  4702  tfisi  4708  findes  4724  relop  4904  dfdmf  4948  dfrnf  4997  resiexg  5082  dfres2  5089  opabresid  5090  mptresid  5091  imai  5117  issref  5144  intasym  5146  cnvi  5166  rnxpid  5196  cnvpom  5304  nfiota1  5313  cbviota  5316  sb8iota  5319  iotaval  5323  iotanul  5327  iota4  5331  eliota  5339  eliotaeu  5340  csbiotag  5344  dffun2  5361  dffun4  5362  dffun5r  5363  dffun6f  5364  dffun4f  5367  sbcfung  5375  funopg  5385  fundif  5399  funinsn  5404  funcnveq  5418  fun11  5422  fununi  5423  funcnvuni  5424  imain  5437  isarep2  5442  brprcneu  5662  fv2  5664  elfv  5667  fv3  5692  relelfvdm  5701  fvmpt2  5760  ralrnmpt  5818  rexrnmpt  5819  ffnfvf  5835  f1veqaeq  5941  dff13f  5942  fliftfuns  5970  canth  6000  cbvriotavw  6013  cbvriota  6014  csbriotag  6016  acexmid  6048  oprabidlem  6080  cbvmpox  6130  cbvmpo  6131  cbvmpov  6132  mpofun  6154  abrexex2  6316  fmpoco  6411  f1o2ndf1  6423  poxp  6427  suppfnss  6456  tposoprab  6510  tfrlem3-2d  6542  tfrlemi1  6562  tfr1onlemsucfn  6570  tfr1onlemaccex  6578  tfrcllemsucfn  6583  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllembfn  6587  tfrcllemaccex  6591  dcdifsnid  6736  fnsnsplitdc  6737  funresdfunsndc  6738  eqerlem  6797  qliftfuns  6852  eroveu  6859  cbvixp  6949  mptelixpg  6968  idssen  7015  modom  7060  pw2f1odclem  7086  xpf1o  7096  xpmapen  7102  findcard2d  7147  fidcen  7155  eqsndc  7162  nnwetri  7175  fiintim  7190  snexxph  7219  fidcenumlemim  7221  fidcenumlemrk  7223  fidcenum  7225  2omap  7268  supmoti  7283  isoti  7297  supisoti  7300  cnvti  7309  ordiso2  7325  ctssdccl  7401  finct  7406  infnninf  7414  nninfwlpoim  7469  nninfwlpo  7471  sspw1or2  7494  exmidontriimlem3  7529  exmidontriimlem4  7530  exmidontriim  7531  onntri13  7547  onntri51  7549  onntri3or  7554  dftap2  7564  netap  7567  2onetap  7568  2omotaplemap  7570  cc1  7578  cc2  7580  ltsopi  7634  addpipqqs  7684  mulpipqqs  7687  archpr  7957  cauappcvgprlemlol  7961  cauappcvgprlemopu  7962  cauappcvgprlemupu  7963  cauappcvgprlemdisj  7965  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  cauappcvgprlemlim  7975  caucvgprlemlol  7984  caucvgprlemopu  7985  caucvgprlemupu  7986  caucvgprlemdisj  7988  caucvgprlemloc  7989  caucvgprlemcl  7990  caucvgprlemladdrl  7992  caucvgprprlemcbv  8001  caucvgprprlemopu  8013  caucvgprprlemclphr  8019  caucvgprprlemexbt  8020  suplocexprlemmu  8032  suplocexprlemdisj  8034  caucvgsrlembound  8108  caucvgsrlembnd  8115  suplocsrlem  8122  suplocsr  8123  peano1nnnn  8166  axcaucvglemres  8213  axpre-suploc  8216  negf1o  8654  lbreu  9218  lbinf  9221  suprubex  9224  suprlubex  9225  suprleubex  9227  1nn  9247  uzind4s  9921  uzind4s2  9922  indstr  9924  supinfneg  9926  infsupneg  9927  infregelbex  9929  eqreznegel  9945  lbzbi  9947  elpq  9980  zsupcl  10590  infssuzex  10592  infssuzledc  10593  zsupssdc  10597  exbtwnzlemex  10608  exbtwnz  10609  rebtwn2zlemstep  10611  rebtwn2z  10613  iseqovex  10819  iseqvalcbv  10820  seqvalcd  10822  seqovcd  10828  seq3f1olemqsum  10874  seq3f1olemp  10876  seq3f1oleml  10877  seqf1og  10882  seq3distr  10893  faclbnd6  11105  fimaxq  11190  hashfibclem  11202  wrd2ind  11411  reuccatpfxs1lem  11434  reuccatpfxs1  11435  cvg1nlemres  11666  resqrexlemsqa  11705  resqrexlemex  11706  cau3lem  11795  fclim  11975  climeu  11977  cn1lem  11995  climcau  12028  climcvg1n  12031  summodclem3  12062  summodclem2a  12063  summodclem2  12064  summodc  12065  zsumdc  12066  fsum3  12069  isumz  12071  isumss2  12075  fsumsersdc  12077  fsum3ser  12079  fsumadd  12088  fsum2dlemstep  12116  fisumcom2  12120  isumshft  12172  cvgratz  12214  mertensabs  12219  prodfdivap  12229  cbvprod  12240  prodmodclem3  12257  prodmodclem2a  12258  prodmodclem2  12259  prodmodc  12260  zproddc  12261  fprodseq  12265  fprodm1s  12283  fprodp1s  12284  fprod2dlemstep  12304  fprodcom2fi  12308  fprodsplitf  12314  odd2np1lem  12554  bitsfzolem  12636  bezoutlemmain  12690  bezoutlemeu  12699  gcdmultiple  12712  rplpwr  12719  nnwofdc  12730  nnwosdc  12731  nninfctlemfo  12732  isprm5lem  12834  isprm5  12835  pw2dvdseu  12861  hashdvds  12914  eulerthlemh  12924  reumodprminv  12947  pclemub  12981  pclemdc  12982  pceu  12989  pcmptdvds  13039  1arith  13061  4sqlem2  13083  4sqlem11  13095  4sqlem12  13096  ennnfonelemg  13146  ennnfoneleminc  13154  ennnfonelemkh  13155  ennnfonelemhf1o  13156  ennnfonelemex  13157  ennnfonelemhom  13158  ennnfonelemrnh  13159  ennnfonelemfun  13160  ennnfonelemdm  13163  ennnfonelemr  13166  ennnfone  13168  inffinp1  13172  ctinf  13173  nninfdclemf  13192  nninfdclemp1  13193  unbendc  13197  infpn2  13199  strsetsid  13237  mgmidmo  13577  lidrididd  13587  mndinvmod  13650  insubm  13690  dfgrp3mlem  13803  mulgaddcom  13855  mulginvcom  13856  isnsg2  13912  gsumfzconstf  14051  srgmulgass  14125  islmodd  14433  lmodvsmmulgdi  14463  rmodislmodlem  14490  rmodislmod  14491  lssats2  14554  mplsubgfilemcl  14846  baspartn  14907  cnpnei  15076  txdis1cn  15135  cnmptid  15138  xmetxp  15364  cncfmptc  15453  cncfmptid  15454  dedekindeulemloc  15476  dedekindicclemloc  15485  ivthinclemlr  15494  ivthinclemur  15496  ivthinclemloc  15498  ivthdec  15501  dvmptfsum  15582  plymullem1  15605  perfectlem2  15860  lgseisenlem2  15936  lgsquadlem3  15944  lgsquad  15945  lgsquad2lem2  15947  2lgslem1a  15953  usgruspgrben  16173  umgr2edg1  16196  umgr2edgneu  16199  usgredg4  16202  usgredgreu  16203  uspgredg2vtxeu  16205  vtxedgfi  16276  vtxlpfi  16277  depindlem1  16493  depindlem2  16494  depindlem3  16495  spimd  16529  2spim  16530  ch2var  16531  bj-sbimedh  16535  bj-sbimeh  16536  cbvrald  16552  sumdc2  16563  bdth  16593  bdcdeq  16601  bdne  16615  bdreu  16617  bdcsn  16632  bdsep2  16648  bdsepnft  16649  bdsepnfALT  16651  bdbm1.3ii  16653  bj-nalset  16657  bj-zfpair2  16672  bj-bdfindes  16711  bj-nn0suc0  16712  bj-nntrans  16713  setindft  16727  setindis  16729  bdsetindis  16731  bj-inf2vnlem3  16734  bj-inf2vnlem4  16735  strcoll2  16745  strcollnft  16746  strcollnfALT  16748  sscoll2  16750  nnti  16758  nnsf  16775  peano4nninf  16776  nninfsellemqall  16785  nninfomni  16789  nnnninfen  16791  repiecef  16804  trilpolemeq1  16816  tridceq  16833  redc0  16834  reap0  16835  dceqnconst  16837  dcapnconst  16838  nconstwlpolemgt0  16841