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  8673  lbreu  9239  lbinf  9242  suprubex  9245  suprlubex  9246  suprleubex  9248  1nn  9268  zfidc  9676  uzind4s  9943  uzind4s2  9944  indstr  9946  supinfneg  9948  infsupneg  9949  infregelbex  9951  eqreznegel  9967  lbzbi  9969  elpq  10002  zsupcl  10616  infssuzex  10618  infssuzledc  10619  zsupssdc  10625  exbtwnzlemex  10636  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  iseqovex  10847  iseqvalcbv  10848  seqvalcd  10850  seqovcd  10856  seq3f1olemqsum  10902  seq3f1olemp  10904  seq3f1oleml  10905  seqf1og  10910  seq3distr  10921  faclbnd6  11134  fimaxq  11222  hashfibclem  11234  wrd2ind  11443  reuccatpfxs1lem  11466  reuccatpfxs1  11467  cvg1nlemres  11699  resqrexlemsqa  11738  resqrexlemex  11739  cau3lem  11828  fclim  12008  climeu  12010  cn1lem  12028  climcau  12061  climcvg1n  12064  summodclem3  12095  summodclem2a  12096  summodclem2  12097  summodc  12098  zsumdc  12099  fsum3  12102  isumz  12104  isumss2  12108  fsumsersdc  12110  fsum3ser  12112  fsumadd  12121  fsum2dlemstep  12149  fisumcom2  12153  isumshft  12205  cvgratz  12247  mertensabs  12252  prodfdivap  12262  cbvprod  12273  prodmodclem3  12290  prodmodclem2a  12291  prodmodclem2  12292  prodmodc  12293  zproddc  12294  fprodseq  12298  fprodm1s  12316  fprodp1s  12317  fprod2dlemstep  12337  fprodcom2fi  12341  fprodsplitf  12347  odd2np1lem  12587  bitsfzolem  12669  bezoutlemmain  12723  bezoutlemeu  12732  gcdmultiple  12745  rplpwr  12752  nnwofdc  12763  nnwosdc  12764  nninfctlemfo  12765  isprm5lem  12867  isprm5  12868  pw2dvdseu  12894  hashdvds  12947  eulerthlemh  12957  reumodprminv  12980  pclemub  13014  pclemdc  13015  pceu  13022  pcmptdvds  13072  1arith  13094  4sqlem2  13116  4sqlem11  13128  4sqlem12  13129  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemefi  13185  ballotfilemodife  13188  ennnfonelemg  13242  ennnfoneleminc  13250  ennnfonelemkh  13251  ennnfonelemhf1o  13252  ennnfonelemex  13253  ennnfonelemhom  13254  ennnfonelemrnh  13255  ennnfonelemfun  13256  ennnfonelemdm  13259  ennnfonelemr  13262  ennnfone  13264  inffinp1  13268  ctinf  13269  nninfdclemf  13288  nninfdclemp1  13289  unbendc  13293  infpn2  13295  strsetsid  13333  mgmidmo  13639  lidrididd  13649  mndinvmod  13710  insubm  13744  dfgrp3mlem  13857  mulgaddcom  13903  mulginvcom  13904  isnsg2  13960  gsumfzconstf  14099  srgmulgass  14236  islmodd  14571  lmodvsmmulgdi  14601  rmodislmodlem  14628  rmodislmod  14629  lssats2  14692  mplsubgfilemcl  14984  baspartn  15045  cnpnei  15214  txdis1cn  15273  cnmptid  15276  xmetxp  15502  cncfmptc  15591  cncfmptid  15592  dedekindeulemloc  15614  dedekindicclemloc  15623  ivthinclemlr  15632  ivthinclemur  15634  ivthinclemloc  15636  ivthdec  15639  dvmptfsum  15720  plymullem1  15743  perfectlem2  15998  lgseisenlem2  16074  lgsquadlem3  16082  lgsquad  16083  lgsquad2lem2  16085  2lgslem1a  16091  usgruspgrben  16311  umgr2edg1  16334  umgr2edgneu  16337  usgredg4  16340  usgredgreu  16341  uspgredg2vtxeu  16343  vtxedgfi  16414  vtxlpfi  16415  depindlem1  16631  depindlem2  16632  depindlem3  16633  spimd  16677  2spim  16678  ch2var  16679  bj-sbimedh  16683  bj-sbimeh  16684  cbvrald  16700  sumdc2  16711  bdth  16741  bdcdeq  16749  bdne  16763  bdreu  16765  bdcsn  16780  bdsep2  16796  bdsepnft  16797  bdsepnfALT  16799  bdbm1.3ii  16801  bj-nalset  16805  bj-zfpair2  16820  bj-bdfindes  16859  bj-nn0suc0  16860  bj-nntrans  16861  setindft  16875  setindis  16877  bdsetindis  16879  bj-inf2vnlem3  16882  bj-inf2vnlem4  16883  strcoll2  16893  strcollnft  16894  strcollnfALT  16896  sscoll2  16898  nnti  16906  nnsf  16923  peano4nninf  16924  nninfsellemqall  16933  nninfomni  16937  nnnninfen  16939  repiecef  16952  trilpolemeq1  16964  tridceq  16981  redc0  16982  reap0  16983  dceqnconst  16985  dcapnconst  16986  nconstwlpolemgt0  16989