Theorem weq 1556

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

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

This proof depends on syntax axioms:   = wceq 1402

This theorem is used by:  alequcoms  1569  equidqe  1585  ax4sp1  1586  spimfv  1751  chvarfv  1752  equid  1753  nfequid  1754  stdpc6  1755  equcomi  1756  ax6evr  1757  equcom  1758  equcomd  1759  equcoms  1760  equtr  1761  equtrr  1762  equtr2  1763  equequ1  1764  equequ2  1765  ax11i  1766  ax10o  1767  ax10  1769  nfae  1771  hbaes  1772  hbnae  1773  nfnae  1774  hbnaes  1775  equsalh  1778  equsal  1779  dral1  1783  dral2  1784  drex2  1785  drnf1  1786  drnf2  1787  spimth  1788  spimh  1790  spimed  1793  cbv1  1798  cbv1h  1799  cbv1v  1800  cbv2h  1801  cbv2w  1803  cbvalv1  1804  cbvexv1  1805  cbvalh  1806  chvar  1810  sbimi  1817  sb1  1819  sb2  1820  sbequ1  1821  sbequ2  1822  sbequ12  1824  sbequ12r  1825  sbequ12a  1826  sbid  1827  stdpc4  1828  sbh  1829  sb6x  1832  sbequ5  1835  sbequ6  1836  equsb1  1838  equsb2  1839  sbiedh  1840  sbiedv  1842  sbieh  1843  equsalv  1846  equs5a  1847  drsb1  1852  exdistrfor  1853  sb4a  1854  equs45f  1855  sb6f  1856  sb5f  1857  sb4e  1858  hbsb2a  1859  hbsb2e  1860  sbcof2  1863  aev  1865  ax16  1866  dveeq2  1868  dveeq2or  1869  ax11v2  1873  ax11a2  1874  ax11b  1879  equs5  1882  equs5or  1883  sb3  1884  sb4  1885  sb4or  1886  sb4b  1887  sb4bor  1888  hbsb2  1889  nfsb2or  1890  sbequi  1892  sbequ  1893  drsb2  1894  spsbe  1895  spsbim  1896  sbequ8  1900  sbidm  1904  sb5rf  1905  sb6rf  1906  ax16i  1911  spv  1913  speiv  1915  equvin  1916  a16g  1917  a16gb  1918  a16nf  1919  equsv  1938  sb56  1940  sb6  1941  sb5  1942  sbnv  1943  sbanv  1944  sborv  1945  sbi1v  1946  sbi2v  1947  cbvalvw  1975  cbvexvw  1976  cbval2  1977  cbvex2  1978  cbvaldva  1984  cbvexdva  1985  cbvaldvaw  1986  cbval2vw  1988  cbvex2vw  1989  cbvex4v  1990  hbs1  1998  hbsbv  2001  nfsbxy  2002  nfsbxyt  2003  nfsbv  2007  equsb3  2011  sbco  2028  sbcocom  2030  sbcomxyyz  2032  sb9v  2038  2sb5  2043  2sb6  2044  sbcom2v  2045  sb6a  2048  2sb5rf  2049  2sb6rf  2050  dfsb7  2051  sb7f  2052  sb7af  2053  sb10f  2055  sbel2x  2058  sbalyz  2059  sbal1yz  2061  sbal1  2062  sbexyz  2063  exsb  2068  2exsb  2069  dvelimALT  2070  dvelimfv  2071  hbsb4t  2073  nfsb4t  2074  dvelimf  2075  dvelimdf  2076  dvelimor  2078  dveeq1  2079  sbal2  2080  euf  2091  eubidh  2092  eubid  2093  hbeu1  2096  nfeu1  2097  sb8eu  2099  nfeuv  2104  sb8euh  2109  eu1  2111  mo2n  2114  euex  2116  eumo0  2117  mo23  2128  mor  2129  modc  2130  eu2  2131  eu3h  2132  mo2r  2139  mo3h  2140  mo2dc  2142  mo4f  2147  eu4  2149  moim  2151  moimv  2153  moanim  2161  mopick  2165  2eu4  2180  euequ1  2182  exists1  2183  elequ1  2213  elequ2  2214  cleljust  2215  elsb1  2216  elsb2  2217  axext3  2221  axext4  2222  bm1.1  2223  eleq1w  2299  cleqh  2338  abbib  2356  cbvabw  2363  cbvab  2364  sbab  2368  nfcjust  2380  drnfc1  2409  drnfc2  2410  nfabdw  2411  dvelimdc  2413  dvelimc  2414  nfcvf  2415  cbvrmow  2735  cbvralfw  2775  cbvrexfw  2776  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralvw  2790  cbvrexvw  2791  cbvreuvw  2792  cbvraldva2  2793  cbvrexdva2  2794  cbvraldva  2795  cbvrexdva  2796  cbvral2vw  2797  cbvrex2vw  2798  cbvral2v  2799  cbvrex2v  2800  cbvral3v  2801  sbralie  2804  cbvrab  2819  vjust  2822  vex  2824  rr19.3v  2965  rr19.28v  2966  ralab2  2990  rexab2  2992  reu2  3014  reu6  3015  reu3  3016  rmo4  3019  reu4  3020  reu7  3021  reu8  3022  rmo3f  3023  rmo4f  3024  cdeqi  3036  cdeqri  3037  cdeqth  3038  cdeqnot  3039  cdeqal  3040  cdeqab  3041  cdeqim  3044  cdeqcv  3045  cdeqeq  3046  cdeqel  3047  nfccdeq  3049  sbsbc  3055  sbc8g  3059  sbcco2  3074  sbc5  3075  sbcralt  3128  sbcralg  3130  sbcreug  3132  reu8nf  3133  rmo3  3144  cbvcsbw  3151  cbvcsb  3152  csbcow  3158  sbcel12g  3162  sbceqg  3163  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  difjust  3221  unjust  3223  injust  3225  dfssf  3238  dfss2f  3239  dfdif3  3339  dfnul2  3523  dfif3  3654  rabsnifsb  3777  preq12bg  3898  eluniab  3947  elintab  3981  int0  3984  dfiunv2  4048  cbviun  4049  cbviin  4050  cbvdisj  4116  invdisjrab  4124  disjiun  4125  sndisj  4126  sbcbrg  4186  cbvmptf  4227  cbvmpt  4228  axsepg  4252  bm1.3ii  4256  nalset  4265  zfpow  4314  el  4317  dtruarb  4330  copsexg  4386  opelopabsb  4404  swopo  4453  pofun  4459  issod  4466  frind  4499  zfun  4581  ruv  4699  dtru  4709  dcextest  4730  tfisi  4736  findes  4752  relop  4932  dfdmf  4976  dfrnf  5025  resiexg  5111  dfres2  5118  opabresid  5119  mptresid  5120  imai  5146  issref  5173  intasym  5175  cnvi  5195  rnxpid  5225  cnvpom  5333  nfiota1  5342  cbviota  5345  sb8iota  5348  iotaval  5352  iotanul  5356  iota4  5360  eliota  5368  eliotaeu  5369  csbiotag  5373  dffun2  5390  dffun4  5391  dffun5r  5392  dffun6f  5393  dffun4f  5396  sbcfung  5404  funopg  5414  fundif  5428  funinsn  5433  funcnveq  5447  fun11  5451  fununi  5452  funcnvuni  5453  imain  5466  isarep2  5471  brprcneu  5691  fv2  5693  elfv  5696  fv3  5721  relelfvdm  5730  fvmpt2  5792  ralrnmpt  5853  rexrnmpt  5854  ffnfvf  5870  f1veqaeq  5978  dff13f  5979  fliftfuns  6007  canth  6039  cbvriotavw  6052  cbvriota  6053  csbriotag  6055  acexmid  6087  oprabidlem  6119  cbvmpox  6169  cbvmpo  6170  cbvmpov  6171  mpofun  6193  abrexex2  6357  fmpoco  6456  f1o2ndf1  6468  poxp  6472  suppfnss  6501  tposoprab  6556  tfrlem3-2d  6588  tfrlemi1  6608  tfr1onlemsucfn  6616  tfr1onlemaccex  6624  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  dcdifsnid  6782  fnsnsplitdc  6783  funresdfunsndc  6784  eqerlem  6843  qliftfuns  6898  eroveu  6905  cbvixp  7003  mptelixpg  7022  idssen  7069  modom  7114  pw2f1odclem  7140  xpf1o  7150  xpmapen  7156  findcard2d  7201  fidcen  7209  eqsndc  7216  nnwetri  7229  fiintim  7244  snexxph  7274  fidcenumlemim  7276  fidcenumlemrk  7278  fidcenum  7280  2omap  7325  supmoti  7340  isoti  7354  supisoti  7357  cnvti  7366  ordiso2  7382  ctssdccl  7458  finct  7463  infnninf  7471  nninfwlpoim  7526  nninfwlpo  7528  sspw1or2  7551  exmidontriimlem3  7586  exmidontriimlem4  7587  exmidontriim  7588  onntri13  7604  onntri51  7606  onntri3or  7611  tapap  7623  dftap2  7624  netap  7627  2onetap  7628  2omotaplemap  7630  cc1  7638  cc2  7640  ltsopi  7694  addpipqqs  7744  mulpipqqs  7747  archpr  8017  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemupu  8023  cauappcvgprlemdisj  8025  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  cauappcvgprlemlim  8035  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemupu  8046  caucvgprlemdisj  8048  caucvgprlemloc  8049  caucvgprlemcl  8050  caucvgprlemladdrl  8052  caucvgprprlemcbv  8061  caucvgprprlemopu  8073  caucvgprprlemclphr  8079  caucvgprprlemexbt  8080  suplocexprlemmu  8092  suplocexprlemdisj  8094  caucvgsrlembound  8168  caucvgsrlembnd  8175  suplocsrlem  8182  suplocsr  8183  peano1nnnn  8226  axcaucvglemres  8273  axpre-suploc  8276  negf1o  8717  lbreu  9284  lbinf  9287  suprubex  9290  suprlubex  9291  suprleubex  9293  1nn  9325  zfidc  9733  fcdmnn0fsuppfi  9744  uzind4s  10006  uzind4s2  10007  indstr  10009  supinfneg  10011  infsupneg  10012  infregelbex  10014  eqreznegel  10030  lbzbi  10032  elpq  10066  zsupcl  10681  infssuzex  10683  infssuzledc  10684  zsupssdc  10690  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  iseqovex  10916  iseqvalcbv  10917  seqvalcd  10919  seqovcd  10925  seq3f1olemqsum  10971  seq3f1olemp  10973  seq3f1oleml  10974  seqf1og  10979  seq3distr  10990  faclbnd6  11204  fimaxq  11292  hashfibclem  11304  hashf1lem1  11307  wrd2ind  11517  reuccatpfxs1lem  11540  reuccatpfxs1  11541  cvg1nlemres  11773  resqrexlemsqa  11812  resqrexlemex  11813  cau3lem  11903  fclim  12085  climeu  12087  cn1lem  12105  climcau  12138  climcvg1n  12141  summodclem3  12172  summodclem2a  12173  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3  12179  isumz  12181  isumss2  12185  fsumsersdc  12187  fsum3ser  12189  fsumadd  12198  fsum2dlemstep  12226  fisumcom2  12230  isumshft  12282  cvgratz  12324  mertensabs  12329  prodfdivap  12339  cbvprod  12350  prodmodclem3  12367  prodmodclem2a  12368  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodm1s  12393  fprodp1s  12394  fprod2dlemstep  12414  fprodcom2fi  12418  fprodsplitf  12424  odd2np1lem  12664  bitsfzolem  12746  bezoutlemmain  12800  bezoutlemeu  12809  gcdmultiple  12822  rplpwr  12829  nnwofdc  12840  nnwosdc  12841  nninfctlemfo  12842  isprm5lem  12945  isprm5  12946  pwbdvdseu  12972  hashdvds  13028  eulerthlemh  13038  reumodprminv  13061  pclemub  13095  pclemdc  13096  pceu  13103  pcmptdvds  13153  1arith  13175  4sqlem2  13197  4sqlem11  13209  4sqlem12  13210  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemefi  13295  ballotfilemodife  13298  ennnfonelemg  13352  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemrnh  13365  ennnfonelemfun  13366  ennnfonelemdm  13369  ennnfonelemr  13372  ennnfone  13374  inffinp1  13378  ctinf  13379  nninfdclemf  13398  nninfdclemp1  13399  unbendc  13403  infpn2  13405  strsetsid  13443  mgmidmo  13751  lidrididd  13761  mndinvmod  13817  insubm  13851  dfgrp3mlem  13962  mulgaddcom  14008  mulginvcom  14009  isnsg2  14065  gzsumconstf  14234  gsum2dfilem2  14272  gsum2d2fi  14274  gsumcom2fi  14275  srgmulgass  14400  islmodd  14738  lmodvsmmulgdi  14769  rmodislmodlem  14796  rmodislmod  14797  lssats2  14860  assamulgscm  15152  psrbagmaxlem1x  15188  psrbagmaxlem1y  15189  psrbagmax  15190  psrlidmfi  15219  psrridmfi  15220  baspartn  15309  cnpnei  15478  txdis1cn  15537  cnmptid  15540  xmetxp  15766  cncfmptc  15855  cncfmptid  15856  dedekindeulemloc  15878  dedekindicclemloc  15887  ivthinclemlr  15896  ivthinclemur  15898  ivthinclemloc  15900  ivthdec  15903  dvmptfsum  15984  plymullem1  16007  zprmlogbap  16251  perfectlem2  16333  bposlem5  16348  lgseisenlem2  16428  lgsquadlem3  16436  lgsquad  16437  lgsquad2lem2  16439  2lgslem1a  16445  usgruspgrben  16665  umgr2edg1  16688  umgr2edgneu  16691  usgredg4  16694  usgredgreu  16695  uspgredg2vtxeu  16697  vtxedgfi  16768  vtxlpfi  16769  depindlem1  16985  depindlem2  16986  depindlem3  16987  spimd  17031  2spim  17032  ch2var  17033  bj-sbimedh  17037  bj-sbimeh  17038  cbvrald  17054  sumdc2  17065  bdth  17095  bdcdeq  17103  bdne  17117  bdreu  17119  bdcsn  17134  bdsep2  17150  bdsepnft  17151  bdsepnfALT  17153  bdbm1.3ii  17155  bj-nalset  17159  bj-zfpair2  17174  bj-bdfindes  17213  bj-nn0suc0  17214  bj-nntrans  17215  setindft  17229  setindis  17231  bdsetindis  17233  bj-inf2vnlem3  17236  bj-inf2vnlem4  17237  strcoll2  17247  strcollnft  17248  strcollnfALT  17250  sscoll2  17252  nnti  17260  nnsf  17287  peano4nninf  17288  nninfsellemqall  17297  nninfomni  17301  nnnninfen  17303  repiecef  17316  trilpolemeq1  17329  tridceq  17346  redc0  17347  reap0  17348  dceqnconst  17350  dcapnconst  17351  nconstwlpolemgt0  17354  cbvals  17386