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 x = y

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1348	1 wff x = y

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  3538  preq12bg  3758  eluniab  3806  elintab  3840  int0  3843  dfiunv2  3907  cbviun  3908  cbviin  3909  cbvdisj  3974  disjiun  3982  sndisj  3983  sbcbrg  4041  cbvmptf  4081  cbvmpt  4082  axsep2  4106  bm1.3ii  4108  nalset  4117  zfpow  4159  el  4162  dtruarb  4175  copsexg  4227  opelopabsb  4243  swopo  4289  pofun  4295  issod  4302  frind  4335  zfun  4417  ruv  4532  dtru  4542  dcextest  4563  tfisi  4569  findes  4585  relop  4759  dfdmf  4802  dfrnf  4850  resiexg  4934  dfres2  4941  opabresid  4942  mptresid  4943  imai  4965  issref  4991  intasym  4993  cnvi  5013  rnxpid  5043  cnvpom  5151  nfiota1  5160  cbviota  5163  sb8iota  5165  iotaval  5169  iotanul  5173  iota4  5176  eliota  5184  eliotaeu  5185  csbiotag  5189  dffun2  5206  dffun4  5207  dffun5r  5208  dffun6f  5209  dffun4f  5212  sbcfung  5220  funopg  5230  funinsn  5245  funcnveq  5259  fun11  5263  fununi  5264  funcnvuni  5265  imain  5278  isarep2  5283  brprcneu  5487  fv2  5489  elfv  5492  fv3  5517  relelfvdm  5526  fvmpt2  5577  ralrnmpt  5635  rexrnmpt  5636  ffnfvf  5652  f1veqaeq  5745  dff13f  5746  fliftfuns  5774  canth  5804  cbvriota  5816  csbriotag  5818  acexmid  5849  oprabidlem  5881  cbvmpox  5928  cbvmpo  5929  cbvmpov  5930  mpofun  5952  abrexex2  6100  fmpoco  6192  f1o2ndf1  6204  poxp  6208  tposoprab  6256  tfrlem3-2d  6288  tfrlemi1  6308  tfr1onlemsucfn  6316  tfr1onlemaccex  6324  tfrcllemsucfn  6329  tfrcllemsucaccv  6330  tfrcllembxssdm  6332  tfrcllembfn  6333  tfrcllemaccex  6337  dcdifsnid  6480  fnsnsplitdc  6481  funresdfunsndc  6482  eqerlem  6540  qliftfuns  6593  eroveu  6600  cbvixp  6689  mptelixpg  6708  idssen  6751  xpf1o  6818  xpmapen  6824  findcard2d  6865  nnwetri  6889  fiintim  6902  snexxph  6923  fidcenumlemim  6925  fidcenumlemrk  6927  fidcenum  6929  supmoti  6966  isoti  6980  supisoti  6983  cnvti  6992  ordiso2  7008  ctssdccl  7084  finct  7089  infnninf  7096  exmidontriimlem3  7187  exmidontriimlem4  7188  exmidontriim  7189  onntri13  7202  onntri51  7204  onntri3or  7209  cc1  7214  cc2  7216  ltsopi  7269  addpipqqs  7319  mulpipqqs  7322  archpr  7592  cauappcvgprlemlol  7596  cauappcvgprlemopu  7597  cauappcvgprlemupu  7598  cauappcvgprlemdisj  7600  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlemlim  7610  caucvgprlemlol  7619  caucvgprlemopu  7620  caucvgprlemupu  7621  caucvgprlemdisj  7623  caucvgprlemloc  7624  caucvgprlemcl  7625  caucvgprlemladdrl  7627  caucvgprprlemcbv  7636  caucvgprprlemopu  7648  caucvgprprlemclphr  7654  caucvgprprlemexbt  7655  suplocexprlemmu  7667  suplocexprlemdisj  7669  caucvgsrlembound  7743  caucvgsrlembnd  7750  suplocsrlem  7757  suplocsr  7758  peano1nnnn  7801  axcaucvglemres  7848  axpre-suploc  7851  negf1o  8288  lbreu  8848  lbinf  8851  suprubex  8854  suprlubex  8855  suprleubex  8857  1nn  8876  uzind4s  9536  uzind4s2  9537  indstr  9539  supinfneg  9541  infsupneg  9542  infregelbex  9544  eqreznegel  9560  lbzbi  9562  elpq  9594  exbtwnzlemex  10193  exbtwnz  10194  rebtwn2zlemstep  10196  rebtwn2z  10198  iseqovex  10399  iseqvalcbv  10400  seqvalcd  10402  seqovcd  10406  seq3f1olemqsum  10443  seq3f1olemp  10445  seq3f1oleml  10446  seq3distr  10456  faclbnd6  10665  fimaxq  10749  cvg1nlemres  10936  resqrexlemsqa  10975  resqrexlemex  10976  cau3lem  11065  fclim  11244  climeu  11246  cn1lem  11264  climcau  11297  climcvg1n  11300  summodclem3  11330  summodclem2a  11331  summodclem2  11332  summodc  11333  zsumdc  11334  fsum3  11337  isumz  11339  isumss2  11343  fsumsersdc  11345  fsum3ser  11347  fsumadd  11356  fsum2dlemstep  11384  fisumcom2  11388  isumshft  11440  cvgratz  11482  mertensabs  11487  prodfdivap  11497  cbvprod  11508  prodmodclem3  11525  prodmodclem2a  11526  prodmodclem2  11527  prodmodc  11528  zproddc  11529  fprodseq  11533  fprodm1s  11551  fprodp1s  11552  fprod2dlemstep  11572  fprodcom2fi  11576  fprodsplitf  11582  odd2np1lem  11818  zsupcl  11889  infssuzex  11891  infssuzledc  11892  zsupssdc  11896  bezoutlemmain  11940  bezoutlemeu  11949  gcdmultiple  11962  rplpwr  11969  nnwofdc  11980  nnwosdc  11981  isprm5lem  12082  isprm5  12083  pw2dvdseu  12109  hashdvds  12162  eulerthlemh  12172  reumodprminv  12194  pclemub  12228  pclemdc  12229  pceu  12236  pcmptdvds  12284  1arith  12306  4sqlem2  12328  ennnfonelemg  12345  ennnfoneleminc  12353  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemrnh  12358  ennnfonelemfun  12359  ennnfonelemdm  12362  ennnfonelemr  12365  ennnfone  12367  inffinp1  12371  ctinf  12372  nninfdclemf  12391  nninfdclemp1  12392  unbendc  12396  infpn2  12398  strsetsid  12436  mgmidmo  12612  lidrididd  12622  mndinvmod  12664  insubm  12689  baspartn  12763  cnpnei  12934  txdis1cn  12993  cnmptid  12996  xmetxp  13222  cncfmptc  13297  cncfmptid  13298  dedekindeulemloc  13312  dedekindicclemloc  13321  ivthinclemlr  13330  ivthinclemur  13332  ivthinclemloc  13334  ivthdec  13337  spimd  13721  2spim  13722  ch2var  13723  bj-sbimedh  13727  bj-sbimeh  13728  cbvrald  13744  sumdc2  13755  bdth  13788  bdcdeq  13796  bdne  13810  bdreu  13812  bdcsn  13827  bdsep2  13843  bdsepnft  13844  bdsepnfALT  13846  bdbm1.3ii  13848  bj-nalset  13852  bj-zfpair2  13867  bj-bdfindes  13906  bj-nn0suc0  13907  bj-nntrans  13908  setindft  13922  setindis  13924  bdsetindis  13926  bj-inf2vnlem3  13929  bj-inf2vnlem4  13930  strcoll2  13940  strcollnft  13941  strcollnfALT  13943  sscoll2  13945  nnti  13949  nnsf  13960  peano4nninf  13961  nninfsellemqall  13970  nninfomni  13974  trilpolemeq1  13994  tridceq  14010  redc0  14011  reap0  14012  dceqnconst  14013  dcapnconst  14014  nconstwlpolemgt0  14017