Theorem weq 1479

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

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

Syntax hints:   = wceq 1331

This theorem is referenced by:  alequcoms  1496  equidqe  1512  ax4sp1  1513  equid  1677  nfequid  1678  stdpc6  1679  equcomi  1680  ax6evr  1681  equcom  1682  equcomd  1683  equcoms  1684  equtr  1685  equtrr  1686  equtr2  1687  equequ1  1688  equequ2  1689  elequ1  1690  elequ2  1691  ax11i  1692  ax10o  1693  ax10  1695  nfae  1697  hbaes  1698  hbnae  1699  nfnae  1700  hbnaes  1701  equsalh  1704  equsal  1705  dral1  1708  dral2  1709  drex2  1710  drnf1  1711  drnf2  1712  spimth  1713  spimh  1715  spimed  1718  cbv1  1722  cbv1h  1723  cbv2h  1724  cbvalh  1726  chvar  1730  sbimi  1737  sb1  1739  sb2  1740  sbequ1  1741  sbequ2  1742  sbequ12  1744  sbequ12r  1745  sbequ12a  1746  sbid  1747  stdpc4  1748  sbh  1749  sb6x  1752  sbequ5  1755  sbequ6  1756  equsb1  1758  equsb2  1759  sbiedh  1760  sbiedv  1762  sbieh  1763  equs5a  1766  drsb1  1771  exdistrfor  1772  sb4a  1773  equs45f  1774  sb6f  1775  sb5f  1776  sb4e  1777  hbsb2a  1778  hbsb2e  1779  sbcof2  1782  aev  1784  ax16  1785  dveeq2  1787  dveeq2or  1788  ax11v2  1792  ax11a2  1793  ax11b  1798  equs5  1801  equs5or  1802  sb3  1803  sb4  1804  sb4or  1805  sb4b  1806  sb4bor  1807  hbsb2  1808  nfsb2or  1809  sbequi  1811  sbequ  1812  drsb2  1813  spsbe  1814  spsbim  1815  sbequ8  1819  sbidm  1823  sb5rf  1824  sb6rf  1825  ax16i  1830  spv  1832  speiv  1834  equvin  1835  a16g  1836  a16gb  1837  a16nf  1838  sb56  1857  sb6  1858  sb5  1859  sbnv  1860  sbanv  1861  sborv  1862  sbi1v  1863  sbi2v  1864  cbval2  1893  cbvex2  1894  cbvaldva  1900  cbvexdva  1901  cbvex4v  1902  cleljust  1910  hbs1  1911  hbsbv  1914  nfsbxy  1915  nfsbxyt  1916  equsb3  1924  sbco  1941  sbcocom  1943  sbcomxyyz  1945  elsb3  1951  elsb4  1952  sb9v  1953  2sb5  1958  2sb6  1959  sbcom2v  1960  sb6a  1963  2sb5rf  1964  2sb6rf  1965  dfsb7  1966  sb7f  1967  sb7af  1968  sb10f  1970  sbel2x  1973  sbalyz  1974  sbal1yz  1976  sbal1  1977  sbexyz  1978  exsb  1983  2exsb  1984  dvelimALT  1985  dvelimfv  1986  hbsb4t  1988  nfsb4t  1989  dvelimf  1990  dvelimdf  1991  dvelimor  1993  dveeq1  1994  sbal2  1997  euf  2004  eubidh  2005  eubid  2006  hbeu1  2009  nfeu1  2010  sb8eu  2012  nfeuv  2017  sb8euh  2022  eu1  2024  mo2n  2027  euex  2029  eumo0  2030  mo23  2040  mor  2041  modc  2042  eu2  2043  eu3h  2044  mo2r  2051  mo3h  2052  mo2dc  2054  mo4f  2059  eu4  2061  moim  2063  moimv  2065  moanim  2073  mopick  2077  2eu4  2092  euequ1  2094  exists1  2095  axext3  2122  axext4  2123  bm1.1  2124  eleq1w  2200  cleqh  2239  cbvab  2263  sbab  2267  nfcjust  2269  drnfc1  2298  drnfc2  2299  dvelimdc  2301  dvelimc  2302  nfcvf  2303  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvraldva2  2661  cbvrexdva2  2662  cbvraldva  2663  cbvrexdva  2664  cbvral2v  2665  cbvrex2v  2666  cbvral3v  2667  sbralie  2670  cbvrab  2684  vjust  2687  vex  2689  rr19.3v  2823  rr19.28v  2824  ralab2  2848  rexab2  2850  reu2  2872  reu6  2873  reu3  2874  rmo4  2877  reu4  2878  reu7  2879  reu8  2880  rmo3f  2881  rmo4f  2882  cdeqi  2894  cdeqri  2895  cdeqth  2896  cdeqnot  2897  cdeqal  2898  cdeqab  2899  cdeqim  2902  cdeqcv  2903  cdeqeq  2904  cdeqel  2905  nfccdeq  2907  sbsbc  2913  sbc8g  2916  sbcco2  2931  sbc5  2932  sbcralt  2985  sbcralg  2987  sbcreug  2989  rmo3  3000  cbvcsbw  3007  cbvcsb  3008  sbcel12g  3017  sbceqg  3018  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  difjust  3072  unjust  3074  injust  3076  dfss2f  3088  dfdif3  3186  dfnul3  3366  dfif3  3487  preq12bg  3700  eluniab  3748  elintab  3782  int0  3785  dfiunv2  3849  cbviun  3850  cbviin  3851  cbvdisj  3916  disjiun  3924  sndisj  3925  sbcbrg  3982  cbvmptf  4022  cbvmpt  4023  axsep2  4047  bm1.3ii  4049  nalset  4058  zfpow  4099  el  4102  dtruarb  4115  copsexg  4166  opelopabsb  4182  swopo  4228  pofun  4234  issod  4241  frind  4274  zfun  4356  ruv  4465  dtru  4475  dcextest  4495  tfisi  4501  findes  4517  relop  4689  dfdmf  4732  dfrnf  4780  resiexg  4864  dfres2  4871  opabresid  4872  mptresid  4873  imai  4895  issref  4921  intasym  4923  cnvi  4943  rnxpid  4973  cnvpom  5081  nfiota1  5090  cbviota  5093  sb8iota  5095  iotaval  5099  iotanul  5103  iota4  5106  csbiotag  5116  dffun2  5133  dffun4  5134  dffun5r  5135  dffun6f  5136  dffun4f  5139  sbcfung  5147  funopg  5157  funinsn  5172  funcnveq  5186  fun11  5190  fununi  5191  funcnvuni  5192  imain  5205  isarep2  5210  brprcneu  5414  fv2  5416  elfv  5419  fv3  5444  relelfvdm  5453  fvmpt2  5504  ralrnmpt  5562  rexrnmpt  5563  ffnfvf  5579  f1veqaeq  5670  dff13f  5671  fliftfuns  5699  cbvriota  5740  csbriotag  5742  acexmid  5773  oprabidlem  5802  cbvmpox  5849  cbvmpo  5850  cbvmpov  5851  mpofun  5873  abrexex2  6022  fmpoco  6113  f1o2ndf1  6125  poxp  6129  tposoprab  6177  tfrlem3-2d  6209  tfrlemi1  6229  tfr1onlemsucfn  6237  tfr1onlemaccex  6245  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  dcdifsnid  6400  fnsnsplitdc  6401  funresdfunsndc  6402  eqerlem  6460  qliftfuns  6513  eroveu  6520  cbvixp  6609  mptelixpg  6628  idssen  6671  xpf1o  6738  xpmapen  6744  findcard2d  6785  nnwetri  6804  fiintim  6817  snexxph  6838  fidcenumlemim  6840  fidcenumlemrk  6842  fidcenum  6844  supmoti  6880  isoti  6894  supisoti  6897  cnvti  6906  ordiso2  6920  ctssdccl  6996  finct  7001  cc1  7080  cc2  7082  ltsopi  7131  addpipqqs  7181  mulpipqqs  7184  archpr  7454  cauappcvgprlemlol  7458  cauappcvgprlemopu  7459  cauappcvgprlemupu  7460  cauappcvgprlemdisj  7462  cauappcvgprlemladdru  7467  cauappcvgprlemladdrl  7468  cauappcvgprlemlim  7472  caucvgprlemlol  7481  caucvgprlemopu  7482  caucvgprlemupu  7483  caucvgprlemdisj  7485  caucvgprlemloc  7486  caucvgprlemcl  7487  caucvgprlemladdrl  7489  caucvgprprlemcbv  7498  caucvgprprlemopu  7510  caucvgprprlemclphr  7516  caucvgprprlemexbt  7517  suplocexprlemmu  7529  suplocexprlemdisj  7531  caucvgsrlembound  7605  caucvgsrlembnd  7612  suplocsrlem  7619  suplocsr  7620  peano1nnnn  7663  axcaucvglemres  7710  axpre-suploc  7713  negf1o  8147  lbreu  8706  lbinf  8709  suprubex  8712  suprlubex  8713  suprleubex  8715  1nn  8734  uzind4s  9388  uzind4s2  9389  indstr  9391  supinfneg  9393  infsupneg  9394  eqreznegel  9409  lbzbi  9411  exbtwnzlemex  10030  exbtwnz  10031  rebtwn2zlemstep  10033  rebtwn2z  10035  iseqovex  10232  iseqvalcbv  10233  seqvalcd  10235  seqovcd  10239  seq3f1olemqsum  10276  seq3f1olemp  10278  seq3f1oleml  10279  seq3distr  10289  faclbnd6  10493  fimaxq  10576  cvg1nlemres  10760  resqrexlemsqa  10799  resqrexlemex  10800  cau3lem  10889  fclim  11066  climeu  11068  cn1lem  11086  climcau  11119  climcvg1n  11122  summodclem3  11152  summodclem2a  11153  summodclem2  11154  summodc  11155  zsumdc  11156  fsum3  11159  isumz  11161  isumss2  11165  fsumsersdc  11167  fsum3ser  11169  fsumadd  11178  fsum2dlemstep  11206  fisumcom2  11210  isumshft  11262  cvgratz  11304  mertensabs  11309  prodfdivap  11319  cbvprod  11330  prodmodclem3  11347  prodmodclem2a  11348  prodmodclem2  11349  prodmodc  11350  odd2np1lem  11572  zsupcl  11643  infssuzex  11645  infssuzledc  11646  bezoutlemmain  11689  bezoutlemeu  11698  gcdmultiple  11711  rplpwr  11718  pw2dvdseu  11849  hashdvds  11900  ennnfonelemg  11919  ennnfoneleminc  11927  ennnfonelemkh  11928  ennnfonelemhf1o  11929  ennnfonelemex  11930  ennnfonelemhom  11931  ennnfonelemrnh  11932  ennnfonelemfun  11933  ennnfonelemdm  11936  ennnfonelemr  11939  ennnfone  11941  inffinp1  11945  ctinf  11946  strsetsid  11995  baspartn  12220  cnpnei  12391  txdis1cn  12450  cnmptid  12453  xmetxp  12679  cncfmptc  12754  cncfmptid  12755  dedekindeulemloc  12769  dedekindicclemloc  12778  ivthinclemlr  12787  ivthinclemur  12789  ivthinclemloc  12791  ivthdec  12794  spimd  12975  2spim  12976  ch2var  12977  bj-sbimedh  12981  bj-sbimeh  12982  cbvrald  12998  sumdc2  13009  bdth  13032  bdcdeq  13040  bdne  13054  bdreu  13056  bdcsn  13071  bdsep2  13087  bdsepnft  13088  bdsepnfALT  13090  bdbm1.3ii  13092  bj-nalset  13096  bj-zfpair2  13111  bj-bdfindes  13150  bj-nn0suc0  13151  bj-nntrans  13152  setindft  13166  setindis  13168  bdsetindis  13170  bj-inf2vnlem3  13173  bj-inf2vnlem4  13174  strcoll2  13184  strcollnft  13185  strcollnfALT  13187  sscoll2  13189  nnti  13194  nnsf  13202  peano4nninf  13203  nninfsellemqall  13214  nninfomni  13218  trilpolemeq1  13236