Theorem weq 1527

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

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

Syntax hints:   = wceq 1373

This theorem is referenced by:  alequcoms  1540  equidqe  1556  ax4sp1  1557  spimfv  1723  chvarfv  1724  equid  1725  nfequid  1726  stdpc6  1727  equcomi  1728  ax6evr  1729  equcom  1730  equcomd  1731  equcoms  1732  equtr  1733  equtrr  1734  equtr2  1735  equequ1  1736  equequ2  1737  ax11i  1738  ax10o  1739  ax10  1741  nfae  1743  hbaes  1744  hbnae  1745  nfnae  1746  hbnaes  1747  equsalh  1750  equsal  1751  dral1  1754  dral2  1755  drex2  1756  drnf1  1757  drnf2  1758  spimth  1759  spimh  1761  spimed  1764  cbv1  1769  cbv1h  1770  cbv1v  1771  cbv2h  1772  cbv2w  1774  cbvalv1  1775  cbvexv1  1776  cbvalh  1777  chvar  1781  sbimi  1788  sb1  1790  sb2  1791  sbequ1  1792  sbequ2  1793  sbequ12  1795  sbequ12r  1796  sbequ12a  1797  sbid  1798  stdpc4  1799  sbh  1800  sb6x  1803  sbequ5  1806  sbequ6  1807  equsb1  1809  equsb2  1810  sbiedh  1811  sbiedv  1813  sbieh  1814  equsalv  1817  equs5a  1818  drsb1  1823  exdistrfor  1824  sb4a  1825  equs45f  1826  sb6f  1827  sb5f  1828  sb4e  1829  hbsb2a  1830  hbsb2e  1831  sbcof2  1834  aev  1836  ax16  1837  dveeq2  1839  dveeq2or  1840  ax11v2  1844  ax11a2  1845  ax11b  1850  equs5  1853  equs5or  1854  sb3  1855  sb4  1856  sb4or  1857  sb4b  1858  sb4bor  1859  hbsb2  1860  nfsb2or  1861  sbequi  1863  sbequ  1864  drsb2  1865  spsbe  1866  spsbim  1867  sbequ8  1871  sbidm  1875  sb5rf  1876  sb6rf  1877  ax16i  1882  spv  1884  speiv  1886  equvin  1887  a16g  1888  a16gb  1889  a16nf  1890  sb56  1910  sb6  1911  sb5  1912  sbnv  1913  sbanv  1914  sborv  1915  sbi1v  1916  sbi2v  1917  cbvalvw  1944  cbvexvw  1945  cbval2  1946  cbvex2  1947  cbvaldva  1953  cbvexdva  1954  cbvaldvaw  1955  cbval2vw  1957  cbvex2vw  1958  cbvex4v  1959  hbs1  1967  hbsbv  1970  nfsbxy  1971  nfsbxyt  1972  nfsbv  1976  equsb3  1980  sbco  1997  sbcocom  1999  sbcomxyyz  2001  sb9v  2007  2sb5  2012  2sb6  2013  sbcom2v  2014  sb6a  2017  2sb5rf  2018  2sb6rf  2019  dfsb7  2020  sb7f  2021  sb7af  2022  sb10f  2024  sbel2x  2027  sbalyz  2028  sbal1yz  2030  sbal1  2031  sbexyz  2032  exsb  2037  2exsb  2038  dvelimALT  2039  dvelimfv  2040  hbsb4t  2042  nfsb4t  2043  dvelimf  2044  dvelimdf  2045  dvelimor  2047  dveeq1  2048  sbal2  2049  euf  2060  eubidh  2061  eubid  2062  hbeu1  2065  nfeu1  2066  sb8eu  2068  nfeuv  2073  sb8euh  2078  eu1  2080  mo2n  2083  euex  2085  eumo0  2086  mo23  2096  mor  2097  modc  2098  eu2  2099  eu3h  2100  mo2r  2107  mo3h  2108  mo2dc  2110  mo4f  2115  eu4  2117  moim  2119  moimv  2121  moanim  2129  mopick  2133  2eu4  2148  euequ1  2150  exists1  2151  elequ1  2181  elequ2  2182  cleljust  2183  elsb1  2184  elsb2  2185  axext3  2189  axext4  2190  bm1.1  2191  eleq1w  2267  cleqh  2306  cbvabw  2329  cbvab  2330  sbab  2334  nfcjust  2337  drnfc1  2366  drnfc2  2367  nfabdw  2368  dvelimdc  2370  dvelimc  2371  nfcvf  2372  cbvralfw  2729  cbvrexfw  2730  cbvralf  2731  cbvrexf  2732  cbvreu  2737  cbvralvw  2743  cbvrexvw  2744  cbvreuvw  2745  cbvraldva2  2746  cbvrexdva2  2747  cbvraldva  2748  cbvrexdva  2749  cbvral2vw  2750  cbvrex2vw  2751  cbvral2v  2752  cbvrex2v  2753  cbvral3v  2754  sbralie  2757  cbvrab  2771  vjust  2774  vex  2776  rr19.3v  2914  rr19.28v  2915  ralab2  2939  rexab2  2941  reu2  2963  reu6  2964  reu3  2965  rmo4  2968  reu4  2969  reu7  2970  reu8  2971  rmo3f  2972  rmo4f  2973  cdeqi  2985  cdeqri  2986  cdeqth  2987  cdeqnot  2988  cdeqal  2989  cdeqab  2990  cdeqim  2993  cdeqcv  2994  cdeqeq  2995  cdeqel  2996  nfccdeq  2998  sbsbc  3004  sbc8g  3008  sbcco2  3023  sbc5  3024  sbcralt  3077  sbcralg  3079  sbcreug  3081  rmo3  3092  cbvcsbw  3099  cbvcsb  3100  csbcow  3106  sbcel12g  3110  sbceqg  3111  cbvralcsf  3158  cbvrexcsf  3159  cbvreucsf  3160  cbvrabcsf  3161  difjust  3169  unjust  3171  injust  3173  dfss2f  3186  dfdif3  3285  dfnul3  3465  dfif3  3586  preq12bg  3817  eluniab  3865  elintab  3899  int0  3902  dfiunv2  3966  cbviun  3967  cbviin  3968  cbvdisj  4034  invdisjrab  4042  disjiun  4043  sndisj  4044  sbcbrg  4103  cbvmptf  4143  cbvmpt  4144  axsep2  4168  bm1.3ii  4170  nalset  4179  zfpow  4224  el  4227  dtruarb  4240  copsexg  4293  opelopabsb  4311  swopo  4358  pofun  4364  issod  4371  frind  4404  zfun  4486  ruv  4603  dtru  4613  dcextest  4634  tfisi  4640  findes  4656  relop  4833  dfdmf  4877  dfrnf  4925  resiexg  5010  dfres2  5017  opabresid  5018  mptresid  5019  imai  5044  issref  5071  intasym  5073  cnvi  5093  rnxpid  5123  cnvpom  5231  nfiota1  5240  cbviota  5243  sb8iota  5245  iotaval  5249  iotanul  5253  iota4  5257  eliota  5265  eliotaeu  5266  csbiotag  5270  dffun2  5287  dffun4  5288  dffun5r  5289  dffun6f  5290  dffun4f  5293  sbcfung  5301  funopg  5311  fundif  5324  funinsn  5329  funcnveq  5343  fun11  5347  fununi  5348  funcnvuni  5349  imain  5362  isarep2  5367  brprcneu  5579  fv2  5581  elfv  5584  fv3  5609  relelfvdm  5618  fvmpt2  5673  ralrnmpt  5732  rexrnmpt  5733  ffnfvf  5749  f1veqaeq  5848  dff13f  5849  fliftfuns  5877  canth  5907  cbvriota  5920  csbriotag  5922  acexmid  5953  oprabidlem  5985  cbvmpox  6033  cbvmpo  6034  cbvmpov  6035  mpofun  6057  abrexex2  6219  fmpoco  6312  f1o2ndf1  6324  poxp  6328  tposoprab  6376  tfrlem3-2d  6408  tfrlemi1  6428  tfr1onlemsucfn  6436  tfr1onlemaccex  6444  tfrcllemsucfn  6449  tfrcllemsucaccv  6450  tfrcllembxssdm  6452  tfrcllembfn  6453  tfrcllemaccex  6457  dcdifsnid  6600  fnsnsplitdc  6601  funresdfunsndc  6602  eqerlem  6661  qliftfuns  6716  eroveu  6723  cbvixp  6812  mptelixpg  6831  idssen  6878  pw2f1odclem  6943  xpf1o  6953  xpmapen  6959  findcard2d  7000  nnwetri  7025  fiintim  7040  snexxph  7064  fidcenumlemim  7066  fidcenumlemrk  7068  fidcenum  7070  supmoti  7107  isoti  7121  supisoti  7124  cnvti  7133  ordiso2  7149  ctssdccl  7225  finct  7230  infnninf  7238  nninfwlpoim  7293  nninfwlpo  7295  exmidontriimlem3  7348  exmidontriimlem4  7349  exmidontriim  7350  onntri13  7363  onntri51  7365  onntri3or  7370  dftap2  7376  netap  7379  2onetap  7380  2omotaplemap  7382  cc1  7390  cc2  7392  ltsopi  7446  addpipqqs  7496  mulpipqqs  7499  archpr  7769  cauappcvgprlemlol  7773  cauappcvgprlemopu  7774  cauappcvgprlemupu  7775  cauappcvgprlemdisj  7777  cauappcvgprlemladdru  7782  cauappcvgprlemladdrl  7783  cauappcvgprlemlim  7787  caucvgprlemlol  7796  caucvgprlemopu  7797  caucvgprlemupu  7798  caucvgprlemdisj  7800  caucvgprlemloc  7801  caucvgprlemcl  7802  caucvgprlemladdrl  7804  caucvgprprlemcbv  7813  caucvgprprlemopu  7825  caucvgprprlemclphr  7831  caucvgprprlemexbt  7832  suplocexprlemmu  7844  suplocexprlemdisj  7846  caucvgsrlembound  7920  caucvgsrlembnd  7927  suplocsrlem  7934  suplocsr  7935  peano1nnnn  7978  axcaucvglemres  8025  axpre-suploc  8028  negf1o  8467  lbreu  9031  lbinf  9034  suprubex  9037  suprlubex  9038  suprleubex  9040  1nn  9060  uzind4s  9724  uzind4s2  9725  indstr  9727  supinfneg  9729  infsupneg  9730  infregelbex  9732  eqreznegel  9748  lbzbi  9750  elpq  9783  zsupcl  10387  infssuzex  10389  infssuzledc  10390  zsupssdc  10394  exbtwnzlemex  10405  exbtwnz  10406  rebtwn2zlemstep  10408  rebtwn2z  10410  iseqovex  10616  iseqvalcbv  10617  seqvalcd  10619  seqovcd  10625  seq3f1olemqsum  10671  seq3f1olemp  10673  seq3f1oleml  10674  seqf1og  10679  seq3distr  10690  faclbnd6  10902  fimaxq  10985  cvg1nlemres  11346  resqrexlemsqa  11385  resqrexlemex  11386  cau3lem  11475  fclim  11655  climeu  11657  cn1lem  11675  climcau  11708  climcvg1n  11711  summodclem3  11741  summodclem2a  11742  summodclem2  11743  summodc  11744  zsumdc  11745  fsum3  11748  isumz  11750  isumss2  11754  fsumsersdc  11756  fsum3ser  11758  fsumadd  11767  fsum2dlemstep  11795  fisumcom2  11799  isumshft  11851  cvgratz  11893  mertensabs  11898  prodfdivap  11908  cbvprod  11919  prodmodclem3  11936  prodmodclem2a  11937  prodmodclem2  11938  prodmodc  11939  zproddc  11940  fprodseq  11944  fprodm1s  11962  fprodp1s  11963  fprod2dlemstep  11983  fprodcom2fi  11987  fprodsplitf  11993  odd2np1lem  12233  bitsfzolem  12315  bezoutlemmain  12369  bezoutlemeu  12378  gcdmultiple  12391  rplpwr  12398  nnwofdc  12409  nnwosdc  12410  nninfctlemfo  12411  isprm5lem  12513  isprm5  12514  pw2dvdseu  12540  hashdvds  12593  eulerthlemh  12603  reumodprminv  12626  pclemub  12660  pclemdc  12661  pceu  12668  pcmptdvds  12718  1arith  12740  4sqlem2  12762  4sqlem11  12774  4sqlem12  12775  ennnfonelemg  12824  ennnfoneleminc  12832  ennnfonelemkh  12833  ennnfonelemhf1o  12834  ennnfonelemex  12835  ennnfonelemhom  12836  ennnfonelemrnh  12837  ennnfonelemfun  12838  ennnfonelemdm  12841  ennnfonelemr  12844  ennnfone  12846  inffinp1  12850  ctinf  12851  nninfdclemf  12870  nninfdclemp1  12871  unbendc  12875  infpn2  12877  strsetsid  12915  mgmidmo  13254  lidrididd  13264  mndinvmod  13327  insubm  13367  dfgrp3mlem  13480  mulgaddcom  13532  mulginvcom  13533  isnsg2  13589  gsumfzconstf  13728  srgmulgass  13801  islmodd  14105  lmodvsmmulgdi  14135  rmodislmodlem  14162  rmodislmod  14163  lssats2  14226  mplsubgfilemcl  14511  baspartn  14572  cnpnei  14741  txdis1cn  14800  cnmptid  14803  xmetxp  15029  cncfmptc  15118  cncfmptid  15119  dedekindeulemloc  15141  dedekindicclemloc  15150  ivthinclemlr  15159  ivthinclemur  15161  ivthinclemloc  15163  ivthdec  15166  dvmptfsum  15247  plymullem1  15270  perfectlem2  15522  lgseisenlem2  15598  lgsquadlem3  15606  lgsquad  15607  lgsquad2lem2  15609  2lgslem1a  15615  spimd  15815  2spim  15816  ch2var  15817  bj-sbimedh  15821  bj-sbimeh  15822  cbvrald  15838  sumdc2  15849  bdth  15881  bdcdeq  15889  bdne  15903  bdreu  15905  bdcsn  15920  bdsep2  15936  bdsepnft  15937  bdsepnfALT  15939  bdbm1.3ii  15941  bj-nalset  15945  bj-zfpair2  15960  bj-bdfindes  15999  bj-nn0suc0  16000  bj-nntrans  16001  setindft  16015  setindis  16017  bdsetindis  16019  bj-inf2vnlem3  16022  bj-inf2vnlem4  16023  strcoll2  16033  strcollnft  16034  strcollnfALT  16036  sscoll2  16038  nnti  16044  2omap  16047  nnsf  16057  peano4nninf  16058  nninfsellemqall  16067  nninfomni  16071  nnnninfen  16073  trilpolemeq1  16094  tridceq  16110  redc0  16111  reap0  16112  dceqnconst  16114  dcapnconst  16115  nconstwlpolemgt0  16118