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  equsv  1934  sb56  1936  sb6  1937  sb5  1938  sbnv  1939  sbanv  1940  sborv  1941  sbi1v  1942  sbi2v  1943  cbvalvw  1971  cbvexvw  1972  cbval2  1973  cbvex2  1974  cbvaldva  1980  cbvexdva  1981  cbvaldvaw  1982  cbval2vw  1984  cbvex2vw  1985  cbvex4v  1986  hbs1  1994  hbsbv  1997  nfsbxy  1998  nfsbxyt  1999  nfsbv  2003  equsb3  2007  sbco  2024  sbcocom  2026  sbcomxyyz  2028  sb9v  2034  2sb5  2039  2sb6  2040  sbcom2v  2041  sb6a  2044  2sb5rf  2045  2sb6rf  2046  dfsb7  2047  sb7f  2048  sb7af  2049  sb10f  2051  sbel2x  2054  sbalyz  2055  sbal1yz  2057  sbal1  2058  sbexyz  2059  exsb  2064  2exsb  2065  dvelimALT  2066  dvelimfv  2067  hbsb4t  2069  nfsb4t  2070  dvelimf  2071  dvelimdf  2072  dvelimor  2074  dveeq1  2075  sbal2  2076  euf  2087  eubidh  2088  eubid  2089  hbeu1  2092  nfeu1  2093  sb8eu  2095  nfeuv  2100  sb8euh  2105  eu1  2107  mo2n  2110  euex  2112  eumo0  2113  mo23  2124  mor  2125  modc  2126  eu2  2127  eu3h  2128  mo2r  2135  mo3h  2136  mo2dc  2138  mo4f  2143  eu4  2145  moim  2147  moimv  2149  moanim  2157  mopick  2161  2eu4  2176  euequ1  2178  exists1  2179  elequ1  2209  elequ2  2210  cleljust  2211  elsb1  2212  elsb2  2213  axext3  2217  axext4  2218  bm1.1  2219  eleq1w  2295  cleqh  2334  abbib  2352  cbvabw  2359  cbvab  2360  sbab  2364  nfcjust  2374  drnfc1  2403  drnfc2  2404  nfabdw  2405  dvelimdc  2407  dvelimc  2408  nfcvf  2409  cbvrmow  2729  cbvralfw  2769  cbvrexfw  2770  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvralvw  2784  cbvrexvw  2785  cbvreuvw  2786  cbvraldva2  2787  cbvrexdva2  2788  cbvraldva  2789  cbvrexdva  2790  cbvral2vw  2791  cbvrex2vw  2792  cbvral2v  2793  cbvrex2v  2794  cbvral3v  2795  sbralie  2798  cbvrab  2813  vjust  2816  vex  2818  rr19.3v  2959  rr19.28v  2960  ralab2  2984  rexab2  2986  reu2  3008  reu6  3009  reu3  3010  rmo4  3013  reu4  3014  reu7  3015  reu8  3016  rmo3f  3017  rmo4f  3018  cdeqi  3030  cdeqri  3031  cdeqth  3032  cdeqnot  3033  cdeqal  3034  cdeqab  3035  cdeqim  3038  cdeqcv  3039  cdeqeq  3040  cdeqel  3041  nfccdeq  3043  sbsbc  3049  sbc8g  3053  sbcco2  3068  sbc5  3069  sbcralt  3122  sbcralg  3124  sbcreug  3126  reu8nf  3127  rmo3  3138  cbvcsbw  3145  cbvcsb  3146  csbcow  3152  sbcel12g  3156  sbceqg  3157  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  difjust  3215  unjust  3217  injust  3219  dfssf  3232  dfss2f  3233  dfdif3  3333  dfnul3  3515  dfif3  3640  rabsnifsb  3762  preq12bg  3882  eluniab  3931  elintab  3965  int0  3968  dfiunv2  4032  cbviun  4033  cbviin  4034  cbvdisj  4100  invdisjrab  4108  disjiun  4109  sndisj  4110  sbcbrg  4169  cbvmptf  4209  cbvmpt  4210  axsep2  4234  bm1.3ii  4236  nalset  4245  zfpow  4293  el  4296  dtruarb  4309  copsexg  4365  opelopabsb  4383  swopo  4432  pofun  4438  issod  4445  frind  4478  zfun  4560  ruv  4677  dtru  4687  dcextest  4708  tfisi  4714  findes  4730  relop  4910  dfdmf  4954  dfrnf  5003  resiexg  5088  dfres2  5095  opabresid  5096  mptresid  5097  imai  5123  issref  5150  intasym  5152  cnvi  5172  rnxpid  5202  cnvpom  5310  nfiota1  5319  cbviota  5322  sb8iota  5325  iotaval  5329  iotanul  5333  iota4  5337  eliota  5345  eliotaeu  5346  csbiotag  5350  dffun2  5367  dffun4  5368  dffun5r  5369  dffun6f  5370  dffun4f  5373  sbcfung  5381  funopg  5391  fundif  5405  funinsn  5410  funcnveq  5424  fun11  5428  fununi  5429  funcnvuni  5430  imain  5443  isarep2  5448  brprcneu  5668  fv2  5670  elfv  5673  fv3  5698  relelfvdm  5707  fvmpt2  5766  ralrnmpt  5824  rexrnmpt  5825  ffnfvf  5841  f1veqaeq  5948  dff13f  5949  fliftfuns  5977  canth  6009  cbvriotavw  6022  cbvriota  6023  csbriotag  6025  acexmid  6057  oprabidlem  6089  cbvmpox  6139  cbvmpo  6140  cbvmpov  6141  mpofun  6163  abrexex2  6326  fmpoco  6425  f1o2ndf1  6437  poxp  6441  suppfnss  6470  tposoprab  6524  tfrlem3-2d  6556  tfrlemi1  6576  tfr1onlemsucfn  6584  tfr1onlemaccex  6592  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  dcdifsnid  6750  fnsnsplitdc  6751  funresdfunsndc  6752  eqerlem  6811  qliftfuns  6866  eroveu  6873  cbvixp  6963  mptelixpg  6982  idssen  7029  modom  7074  pw2f1odclem  7100  xpf1o  7110  xpmapen  7116  findcard2d  7161  fidcen  7169  eqsndc  7176  nnwetri  7189  fiintim  7204  snexxph  7233  fidcenumlemim  7235  fidcenumlemrk  7237  fidcenum  7239  2omap  7282  supmoti  7297  isoti  7311  supisoti  7314  cnvti  7323  ordiso2  7339  ctssdccl  7415  finct  7420  infnninf  7428  nninfwlpoim  7483  nninfwlpo  7485  sspw1or2  7508  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  onntri13  7561  onntri51  7563  onntri3or  7568  tapap  7580  dftap2  7581  netap  7584  2onetap  7585  2omotaplemap  7587  cc1  7595  cc2  7597  ltsopi  7651  addpipqqs  7701  mulpipqqs  7704  archpr  7974  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlemlim  7992  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdrl  8009  caucvgprprlemcbv  8018  caucvgprprlemopu  8030  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  suplocexprlemmu  8049  suplocexprlemdisj  8051  caucvgsrlembound  8125  caucvgsrlembnd  8132  suplocsrlem  8139  suplocsr  8140  peano1nnnn  8183  axcaucvglemres  8230  axpre-suploc  8233  negf1o  8672  lbreu  9236  lbinf  9239  suprubex  9242  suprlubex  9243  suprleubex  9245  1nn  9265  zfidc  9673  uzind4s  9940  uzind4s2  9941  indstr  9943  supinfneg  9945  infsupneg  9946  infregelbex  9948  eqreznegel  9964  lbzbi  9966  elpq  9999  zsupcl  10613  infssuzex  10615  infssuzledc  10616  zsupssdc  10622  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  iseqovex  10844  iseqvalcbv  10845  seqvalcd  10847  seqovcd  10853  seq3f1olemqsum  10899  seq3f1olemp  10901  seq3f1oleml  10902  seqf1og  10907  seq3distr  10918  faclbnd6  11131  fimaxq  11219  hashfibclem  11231  wrd2ind  11440  reuccatpfxs1lem  11463  reuccatpfxs1  11464  cvg1nlemres  11695  resqrexlemsqa  11734  resqrexlemex  11735  cau3lem  11824  fclim  12004  climeu  12006  cn1lem  12024  climcau  12057  climcvg1n  12060  summodclem3  12091  summodclem2a  12092  summodclem2  12093  summodc  12094  zsumdc  12095  fsum3  12098  isumz  12100  isumss2  12104  fsumsersdc  12106  fsum3ser  12108  fsumadd  12117  fsum2dlemstep  12145  fisumcom2  12149  isumshft  12201  cvgratz  12243  mertensabs  12248  prodfdivap  12258  cbvprod  12269  prodmodclem3  12286  prodmodclem2a  12287  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodm1s  12312  fprodp1s  12313  fprod2dlemstep  12333  fprodcom2fi  12337  fprodsplitf  12343  odd2np1lem  12583  bitsfzolem  12665  bezoutlemmain  12719  bezoutlemeu  12728  gcdmultiple  12741  rplpwr  12748  nnwofdc  12759  nnwosdc  12760  nninfctlemfo  12761  isprm5lem  12863  isprm5  12864  pw2dvdseu  12890  hashdvds  12943  eulerthlemh  12953  reumodprminv  12976  pclemub  13010  pclemdc  13011  pceu  13018  pcmptdvds  13068  1arith  13090  4sqlem2  13112  4sqlem11  13124  4sqlem12  13125  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemefi  13181  ballotfilemodife  13184  ennnfonelemg  13238  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemrnh  13251  ennnfonelemfun  13252  ennnfonelemdm  13255  ennnfonelemr  13258  ennnfone  13260  inffinp1  13264  ctinf  13265  nninfdclemf  13284  nninfdclemp1  13285  unbendc  13289  infpn2  13291  strsetsid  13329  mgmidmo  13669  lidrididd  13679  mndinvmod  13742  insubm  13782  dfgrp3mlem  13895  mulgaddcom  13947  mulginvcom  13948  isnsg2  14004  gsumfzconstf  14143  srgmulgass  14217  islmodd  14553  lmodvsmmulgdi  14583  rmodislmodlem  14610  rmodislmod  14611  lssats2  14674  mplsubgfilemcl  14966  baspartn  15027  cnpnei  15196  txdis1cn  15255  cnmptid  15258  xmetxp  15484  cncfmptc  15573  cncfmptid  15574  dedekindeulemloc  15596  dedekindicclemloc  15605  ivthinclemlr  15614  ivthinclemur  15616  ivthinclemloc  15618  ivthdec  15621  dvmptfsum  15702  plymullem1  15725  perfectlem2  15980  lgseisenlem2  16056  lgsquadlem3  16064  lgsquad  16065  lgsquad2lem2  16067  2lgslem1a  16073  usgruspgrben  16293  umgr2edg1  16316  umgr2edgneu  16319  usgredg4  16322  usgredgreu  16323  uspgredg2vtxeu  16325  vtxedgfi  16396  vtxlpfi  16397  depindlem1  16613  depindlem2  16614  depindlem3  16615  spimd  16649  2spim  16650  ch2var  16651  bj-sbimedh  16655  bj-sbimeh  16656  cbvrald  16672  sumdc2  16683  bdth  16713  bdcdeq  16721  bdne  16735  bdreu  16737  bdcsn  16752  bdsep2  16768  bdsepnft  16769  bdsepnfALT  16771  bdbm1.3ii  16773  bj-nalset  16777  bj-zfpair2  16792  bj-bdfindes  16831  bj-nn0suc0  16832  bj-nntrans  16833  setindft  16847  setindis  16849  bdsetindis  16851  bj-inf2vnlem3  16854  bj-inf2vnlem4  16855  strcoll2  16865  strcollnft  16866  strcollnfALT  16868  sscoll2  16870  nnti  16878  nnsf  16895  peano4nninf  16896  nninfsellemqall  16905  nninfomni  16909  nnnninfen  16911  repiecef  16924  trilpolemeq1  16936  tridceq  16953  redc0  16954  reap0  16955  dceqnconst  16958  dcapnconst  16959  nconstwlpolemgt0  16962