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 𝑥 = 𝑦

Syntax hints:   = wceq 1402

This theorem is referenced 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  3776  preq12bg  3896  eluniab  3945  elintab  3979  int0  3982  dfiunv2  4046  cbviun  4047  cbviin  4048  cbvdisj  4114  invdisjrab  4122  disjiun  4123  sndisj  4124  sbcbrg  4183  cbvmptf  4223  cbvmpt  4224  axsepg  4248  bm1.3ii  4252  nalset  4261  zfpow  4310  el  4313  dtruarb  4326  copsexg  4382  opelopabsb  4400  swopo  4449  pofun  4455  issod  4462  frind  4495  zfun  4577  ruv  4695  dtru  4705  dcextest  4726  tfisi  4732  findes  4748  relop  4928  dfdmf  4972  dfrnf  5021  resiexg  5106  dfres2  5113  opabresid  5114  mptresid  5115  imai  5141  issref  5168  intasym  5170  cnvi  5190  rnxpid  5220  cnvpom  5328  nfiota1  5337  cbviota  5340  sb8iota  5343  iotaval  5347  iotanul  5351  iota4  5355  eliota  5363  eliotaeu  5364  csbiotag  5368  dffun2  5385  dffun4  5386  dffun5r  5387  dffun6f  5388  dffun4f  5391  sbcfung  5399  funopg  5409  fundif  5423  funinsn  5428  funcnveq  5442  fun11  5446  fununi  5447  funcnvuni  5448  imain  5461  isarep2  5466  brprcneu  5686  fv2  5688  elfv  5691  fv3  5716  relelfvdm  5725  fvmpt2  5786  ralrnmpt  5844  rexrnmpt  5845  ffnfvf  5861  f1veqaeq  5969  dff13f  5970  fliftfuns  5998  canth  6030  cbvriotavw  6043  cbvriota  6044  csbriotag  6046  acexmid  6078  oprabidlem  6110  cbvmpox  6160  cbvmpo  6161  cbvmpov  6162  mpofun  6184  abrexex2  6347  fmpoco  6446  f1o2ndf1  6458  poxp  6462  suppfnss  6491  tposoprab  6545  tfrlem3-2d  6577  tfrlemi1  6597  tfr1onlemsucfn  6605  tfr1onlemaccex  6613  tfrcllemsucfn  6618  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllembfn  6622  tfrcllemaccex  6626  dcdifsnid  6771  fnsnsplitdc  6772  funresdfunsndc  6773  eqerlem  6832  qliftfuns  6887  eroveu  6894  cbvixp  6991  mptelixpg  7010  idssen  7057  modom  7102  pw2f1odclem  7128  xpf1o  7138  xpmapen  7144  findcard2d  7189  fidcen  7197  eqsndc  7204  nnwetri  7217  fiintim  7232  snexxph  7261  fidcenumlemim  7263  fidcenumlemrk  7265  fidcenum  7267  2omap  7312  supmoti  7327  isoti  7341  supisoti  7344  cnvti  7353  ordiso2  7369  ctssdccl  7445  finct  7450  infnninf  7458  nninfwlpoim  7513  nninfwlpo  7515  sspw1or2  7538  exmidontriimlem3  7573  exmidontriimlem4  7574  exmidontriim  7575  onntri13  7591  onntri51  7593  onntri3or  7598  tapap  7610  dftap2  7611  netap  7614  2onetap  7615  2omotaplemap  7617  cc1  7625  cc2  7627  ltsopi  7681  addpipqqs  7731  mulpipqqs  7734  archpr  8004  cauappcvgprlemlol  8008  cauappcvgprlemopu  8009  cauappcvgprlemupu  8010  cauappcvgprlemdisj  8012  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  cauappcvgprlemlim  8022  caucvgprlemlol  8031  caucvgprlemopu  8032  caucvgprlemupu  8033  caucvgprlemdisj  8035  caucvgprlemloc  8036  caucvgprlemcl  8037  caucvgprlemladdrl  8039  caucvgprprlemcbv  8048  caucvgprprlemopu  8060  caucvgprprlemclphr  8066  caucvgprprlemexbt  8067  suplocexprlemmu  8079  suplocexprlemdisj  8081  caucvgsrlembound  8155  caucvgsrlembnd  8162  suplocsrlem  8169  suplocsr  8170  peano1nnnn  8213  axcaucvglemres  8260  axpre-suploc  8263  negf1o  8703  lbreu  9269  lbinf  9272  suprubex  9275  suprlubex  9276  suprleubex  9278  1nn  9298  zfidc  9706  uzind4s  9973  uzind4s2  9974  indstr  9976  supinfneg  9978  infsupneg  9979  infregelbex  9981  eqreznegel  9997  lbzbi  9999  elpq  10032  zsupcl  10647  infssuzex  10649  infssuzledc  10650  zsupssdc  10656  exbtwnzlemex  10667  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2z  10672  iseqovex  10878  iseqvalcbv  10879  seqvalcd  10881  seqovcd  10887  seq3f1olemqsum  10933  seq3f1olemp  10935  seq3f1oleml  10936  seqf1og  10941  seq3distr  10952  faclbnd6  11165  fimaxq  11253  hashfibclem  11265  hashf1lem1  11268  wrd2ind  11478  reuccatpfxs1lem  11501  reuccatpfxs1  11502  cvg1nlemres  11734  resqrexlemsqa  11773  resqrexlemex  11774  cau3lem  11863  fclim  12043  climeu  12045  cn1lem  12063  climcau  12096  climcvg1n  12099  summodclem3  12130  summodclem2a  12131  summodclem2  12132  summodc  12133  zsumdc  12134  fsum3  12137  isumz  12139  isumss2  12143  fsumsersdc  12145  fsum3ser  12147  fsumadd  12156  fsum2dlemstep  12184  fisumcom2  12188  isumshft  12240  cvgratz  12282  mertensabs  12287  prodfdivap  12297  cbvprod  12308  prodmodclem3  12325  prodmodclem2a  12326  prodmodclem2  12327  prodmodc  12328  zproddc  12329  fprodseq  12333  fprodm1s  12351  fprodp1s  12352  fprod2dlemstep  12372  fprodcom2fi  12376  fprodsplitf  12382  odd2np1lem  12622  bitsfzolem  12704  bezoutlemmain  12758  bezoutlemeu  12767  gcdmultiple  12780  rplpwr  12787  nnwofdc  12798  nnwosdc  12799  nninfctlemfo  12800  isprm5lem  12902  isprm5  12903  pw2dvdseu  12929  hashdvds  12982  eulerthlemh  12992  reumodprminv  13015  pclemub  13049  pclemdc  13050  pceu  13057  pcmptdvds  13107  1arith  13129  4sqlem2  13151  4sqlem11  13163  4sqlem12  13164  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemefi  13220  ballotfilemodife  13223  ennnfonelemg  13277  ennnfoneleminc  13285  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemex  13288  ennnfonelemhom  13289  ennnfonelemrnh  13290  ennnfonelemfun  13291  ennnfonelemdm  13294  ennnfonelemr  13297  ennnfone  13299  inffinp1  13303  ctinf  13304  nninfdclemf  13323  nninfdclemp1  13324  unbendc  13328  infpn2  13330  strsetsid  13368  mgmidmo  13675  lidrididd  13685  mndinvmod  13741  insubm  13775  dfgrp3mlem  13886  mulgaddcom  13932  mulginvcom  13933  isnsg2  13989  gzsumconstf  14127  srgmulgass  14276  islmodd  14612  lmodvsmmulgdi  14643  rmodislmodlem  14670  rmodislmod  14671  lssats2  14734  assamulgscm  15026  mplsubgfilemcl  15073  baspartn  15134  cnpnei  15303  txdis1cn  15362  cnmptid  15365  xmetxp  15591  cncfmptc  15680  cncfmptid  15681  dedekindeulemloc  15703  dedekindicclemloc  15712  ivthinclemlr  15721  ivthinclemur  15723  ivthinclemloc  15725  ivthdec  15728  dvmptfsum  15809  plymullem1  15832  perfectlem2  16097  lgseisenlem2  16173  lgsquadlem3  16181  lgsquad  16182  lgsquad2lem2  16184  2lgslem1a  16190  usgruspgrben  16410  umgr2edg1  16433  umgr2edgneu  16436  usgredg4  16439  usgredgreu  16440  uspgredg2vtxeu  16442  vtxedgfi  16513  vtxlpfi  16514  depindlem1  16730  depindlem2  16731  depindlem3  16732  spimd  16776  2spim  16777  ch2var  16778  bj-sbimedh  16782  bj-sbimeh  16783  cbvrald  16799  sumdc2  16810  bdth  16840  bdcdeq  16848  bdne  16862  bdreu  16864  bdcsn  16879  bdsep2  16895  bdsepnft  16896  bdsepnfALT  16898  bdbm1.3ii  16900  bj-nalset  16904  bj-zfpair2  16919  bj-bdfindes  16958  bj-nn0suc0  16959  bj-nntrans  16960  setindft  16974  setindis  16976  bdsetindis  16978  bj-inf2vnlem3  16981  bj-inf2vnlem4  16982  strcoll2  16992  strcollnft  16993  strcollnfALT  16995  sscoll2  16997  nnti  17005  nnsf  17022  peano4nninf  17023  nninfsellemqall  17032  nninfomni  17036  nnnninfen  17038  repiecef  17051  trilpolemeq1  17063  tridceq  17080  redc0  17081  reap0  17082  dceqnconst  17084  dcapnconst  17085  nconstwlpolemgt0  17088  cbvals  17120