Theorem weq 1496

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

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

Syntax hints:   = wceq 1348

This theorem is referenced by:  alequcoms  1509  equidqe  1525  ax4sp1  1526  spimfv  1692  chvarfv  1693  equid  1694  nfequid  1695  stdpc6  1696  equcomi  1697  ax6evr  1698  equcom  1699  equcomd  1700  equcoms  1701  equtr  1702  equtrr  1703  equtr2  1704  equequ1  1705  equequ2  1706  ax11i  1707  ax10o  1708  ax10  1710  nfae  1712  hbaes  1713  hbnae  1714  nfnae  1715  hbnaes  1716  equsalh  1719  equsal  1720  dral1  1723  dral2  1724  drex2  1725  drnf1  1726  drnf2  1727  spimth  1728  spimh  1730  spimed  1733  cbv1  1738  cbv1h  1739  cbv1v  1740  cbv2h  1741  cbv2w  1743  cbvalv1  1744  cbvexv1  1745  cbvalh  1746  chvar  1750  sbimi  1757  sb1  1759  sb2  1760  sbequ1  1761  sbequ2  1762  sbequ12  1764  sbequ12r  1765  sbequ12a  1766  sbid  1767  stdpc4  1768  sbh  1769  sb6x  1772  sbequ5  1775  sbequ6  1776  equsb1  1778  equsb2  1779  sbiedh  1780  sbiedv  1782  sbieh  1783  equsalv  1786  equs5a  1787  drsb1  1792  exdistrfor  1793  sb4a  1794  equs45f  1795  sb6f  1796  sb5f  1797  sb4e  1798  hbsb2a  1799  hbsb2e  1800  sbcof2  1803  aev  1805  ax16  1806  dveeq2  1808  dveeq2or  1809  ax11v2  1813  ax11a2  1814  ax11b  1819  equs5  1822  equs5or  1823  sb3  1824  sb4  1825  sb4or  1826  sb4b  1827  sb4bor  1828  hbsb2  1829  nfsb2or  1830  sbequi  1832  sbequ  1833  drsb2  1834  spsbe  1835  spsbim  1836  sbequ8  1840  sbidm  1844  sb5rf  1845  sb6rf  1846  ax16i  1851  spv  1853  speiv  1855  equvin  1856  a16g  1857  a16gb  1858  a16nf  1859  sb56  1878  sb6  1879  sb5  1880  sbnv  1881  sbanv  1882  sborv  1883  sbi1v  1884  sbi2v  1885  cbvalvw  1912  cbvexvw  1913  cbval2  1914  cbvex2  1915  cbvaldva  1921  cbvexdva  1922  cbvex4v  1923  hbs1  1931  hbsbv  1934  nfsbxy  1935  nfsbxyt  1936  nfsbv  1940  equsb3  1944  sbco  1961  sbcocom  1963  sbcomxyyz  1965  sb9v  1971  2sb5  1976  2sb6  1977  sbcom2v  1978  sb6a  1981  2sb5rf  1982  2sb6rf  1983  dfsb7  1984  sb7f  1985  sb7af  1986  sb10f  1988  sbel2x  1991  sbalyz  1992  sbal1yz  1994  sbal1  1995  sbexyz  1996  exsb  2001  2exsb  2002  dvelimALT  2003  dvelimfv  2004  hbsb4t  2006  nfsb4t  2007  dvelimf  2008  dvelimdf  2009  dvelimor  2011  dveeq1  2012  sbal2  2013  euf  2024  eubidh  2025  eubid  2026  hbeu1  2029  nfeu1  2030  sb8eu  2032  nfeuv  2037  sb8euh  2042  eu1  2044  mo2n  2047  euex  2049  eumo0  2050  mo23  2060  mor  2061  modc  2062  eu2  2063  eu3h  2064  mo2r  2071  mo3h  2072  mo2dc  2074  mo4f  2079  eu4  2081  moim  2083  moimv  2085  moanim  2093  mopick  2097  2eu4  2112  euequ1  2114  exists1  2115  elequ1  2145  elequ2  2146  cleljust  2147  elsb1  2148  elsb2  2149  axext3  2153  axext4  2154  bm1.1  2155  eleq1w  2231  cleqh  2270  cbvabw  2293  cbvab  2294  sbab  2298  nfcjust  2300  drnfc1  2329  drnfc2  2330  nfabdw  2331  dvelimdc  2333  dvelimc  2334  nfcvf  2335  cbvralfw  2687  cbvrexfw  2688  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvralvw  2700  cbvrexvw  2701  cbvreuvw  2702  cbvraldva2  2703  cbvrexdva2  2704  cbvraldva  2705  cbvrexdva  2706  cbvral2vw  2707  cbvrex2vw  2708  cbvral2v  2709  cbvrex2v  2710  cbvral3v  2711  sbralie  2714  cbvrab  2728  vjust  2731  vex  2733  rr19.3v  2869  rr19.28v  2870  ralab2  2894  rexab2  2896  reu2  2918  reu6  2919  reu3  2920  rmo4  2923  reu4  2924  reu7  2925  reu8  2926  rmo3f  2927  rmo4f  2928  cdeqi  2940  cdeqri  2941  cdeqth  2942  cdeqnot  2943  cdeqal  2944  cdeqab  2945  cdeqim  2948  cdeqcv  2949  cdeqeq  2950  cdeqel  2951  nfccdeq  2953  sbsbc  2959  sbc8g  2962  sbcco2  2977  sbc5  2978  sbcralt  3031  sbcralg  3033  sbcreug  3035  rmo3  3046  cbvcsbw  3053  cbvcsb  3054  csbcow  3060  sbcel12g  3064  sbceqg  3065  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  difjust  3122  unjust  3124  injust  3126  dfss2f  3138  dfdif3  3237  dfnul3  3417  dfif3  3539  preq12bg  3760  eluniab  3808  elintab  3842  int0  3845  dfiunv2  3909  cbviun  3910  cbviin  3911  cbvdisj  3976  disjiun  3984  sndisj  3985  sbcbrg  4043  cbvmptf  4083  cbvmpt  4084  axsep2  4108  bm1.3ii  4110  nalset  4119  zfpow  4161  el  4164  dtruarb  4177  copsexg  4229  opelopabsb  4245  swopo  4291  pofun  4297  issod  4304  frind  4337  zfun  4419  ruv  4534  dtru  4544  dcextest  4565  tfisi  4571  findes  4587  relop  4761  dfdmf  4804  dfrnf  4852  resiexg  4936  dfres2  4943  opabresid  4944  mptresid  4945  imai  4967  issref  4993  intasym  4995  cnvi  5015  rnxpid  5045  cnvpom  5153  nfiota1  5162  cbviota  5165  sb8iota  5167  iotaval  5171  iotanul  5175  iota4  5178  eliota  5186  eliotaeu  5187  csbiotag  5191  dffun2  5208  dffun4  5209  dffun5r  5210  dffun6f  5211  dffun4f  5214  sbcfung  5222  funopg  5232  funinsn  5247  funcnveq  5261  fun11  5265  fununi  5266  funcnvuni  5267  imain  5280  isarep2  5285  brprcneu  5489  fv2  5491  elfv  5494  fv3  5519  relelfvdm  5528  fvmpt2  5579  ralrnmpt  5638  rexrnmpt  5639  ffnfvf  5655  f1veqaeq  5748  dff13f  5749  fliftfuns  5777  canth  5807  cbvriota  5819  csbriotag  5821  acexmid  5852  oprabidlem  5884  cbvmpox  5931  cbvmpo  5932  cbvmpov  5933  mpofun  5955  abrexex2  6103  fmpoco  6195  f1o2ndf1  6207  poxp  6211  tposoprab  6259  tfrlem3-2d  6291  tfrlemi1  6311  tfr1onlemsucfn  6319  tfr1onlemaccex  6327  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemaccex  6340  dcdifsnid  6483  fnsnsplitdc  6484  funresdfunsndc  6485  eqerlem  6544  qliftfuns  6597  eroveu  6604  cbvixp  6693  mptelixpg  6712  idssen  6755  xpf1o  6822  xpmapen  6828  findcard2d  6869  nnwetri  6893  fiintim  6906  snexxph  6927  fidcenumlemim  6929  fidcenumlemrk  6931  fidcenum  6933  supmoti  6970  isoti  6984  supisoti  6987  cnvti  6996  ordiso2  7012  ctssdccl  7088  finct  7093  infnninf  7100  nninfwlpoim  7154  nninfwlpo  7155  exmidontriimlem3  7200  exmidontriimlem4  7201  exmidontriim  7202  onntri13  7215  onntri51  7217  onntri3or  7222  cc1  7227  cc2  7229  ltsopi  7282  addpipqqs  7332  mulpipqqs  7335  archpr  7605  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlemlim  7623  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdrl  7640  caucvgprprlemcbv  7649  caucvgprprlemopu  7661  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  suplocexprlemmu  7680  suplocexprlemdisj  7682  caucvgsrlembound  7756  caucvgsrlembnd  7763  suplocsrlem  7770  suplocsr  7771  peano1nnnn  7814  axcaucvglemres  7861  axpre-suploc  7864  negf1o  8301  lbreu  8861  lbinf  8864  suprubex  8867  suprlubex  8868  suprleubex  8870  1nn  8889  uzind4s  9549  uzind4s2  9550  indstr  9552  supinfneg  9554  infsupneg  9555  infregelbex  9557  eqreznegel  9573  lbzbi  9575  elpq  9607  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2z  10211  iseqovex  10412  iseqvalcbv  10413  seqvalcd  10415  seqovcd  10419  seq3f1olemqsum  10456  seq3f1olemp  10458  seq3f1oleml  10459  seq3distr  10469  faclbnd6  10678  fimaxq  10762  cvg1nlemres  10949  resqrexlemsqa  10988  resqrexlemex  10989  cau3lem  11078  fclim  11257  climeu  11259  cn1lem  11277  climcau  11310  climcvg1n  11313  summodclem3  11343  summodclem2a  11344  summodclem2  11345  summodc  11346  zsumdc  11347  fsum3  11350  isumz  11352  isumss2  11356  fsumsersdc  11358  fsum3ser  11360  fsumadd  11369  fsum2dlemstep  11397  fisumcom2  11401  isumshft  11453  cvgratz  11495  mertensabs  11500  prodfdivap  11510  cbvprod  11521  prodmodclem3  11538  prodmodclem2a  11539  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodm1s  11564  fprodp1s  11565  fprod2dlemstep  11585  fprodcom2fi  11589  fprodsplitf  11595  odd2np1lem  11831  zsupcl  11902  infssuzex  11904  infssuzledc  11905  zsupssdc  11909  bezoutlemmain  11953  bezoutlemeu  11962  gcdmultiple  11975  rplpwr  11982  nnwofdc  11993  nnwosdc  11994  isprm5lem  12095  isprm5  12096  pw2dvdseu  12122  hashdvds  12175  eulerthlemh  12185  reumodprminv  12207  pclemub  12241  pclemdc  12242  pceu  12249  pcmptdvds  12297  1arith  12319  4sqlem2  12341  ennnfonelemg  12358  ennnfoneleminc  12366  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemrnh  12371  ennnfonelemfun  12372  ennnfonelemdm  12375  ennnfonelemr  12378  ennnfone  12380  inffinp1  12384  ctinf  12385  nninfdclemf  12404  nninfdclemp1  12405  unbendc  12409  infpn2  12411  strsetsid  12449  mgmidmo  12626  lidrididd  12636  mndinvmod  12678  insubm  12703  baspartn  12842  cnpnei  13013  txdis1cn  13072  cnmptid  13075  xmetxp  13301  cncfmptc  13376  cncfmptid  13377  dedekindeulemloc  13391  dedekindicclemloc  13400  ivthinclemlr  13409  ivthinclemur  13411  ivthinclemloc  13413  ivthdec  13416  spimd  13800  2spim  13801  ch2var  13802  bj-sbimedh  13806  bj-sbimeh  13807  cbvrald  13823  sumdc2  13834  bdth  13866  bdcdeq  13874  bdne  13888  bdreu  13890  bdcsn  13905  bdsep2  13921  bdsepnft  13922  bdsepnfALT  13924  bdbm1.3ii  13926  bj-nalset  13930  bj-zfpair2  13945  bj-bdfindes  13984  bj-nn0suc0  13985  bj-nntrans  13986  setindft  14000  setindis  14002  bdsetindis  14004  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008  strcoll2  14018  strcollnft  14019  strcollnfALT  14021  sscoll2  14023  nnti  14027  nnsf  14038  peano4nninf  14039  nninfsellemqall  14048  nninfomni  14052  trilpolemeq1  14072  tridceq  14088  redc0  14089  reap0  14090  dceqnconst  14091  dcapnconst  14092  nconstwlpolemgt0  14095