Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  weq GIF version

Theorem weq 1480
 Description: Extend wff definition to include atomic formulas using the equality predicate. (Instead of introducing weq 1480 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 1332. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1480 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1332. 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
StepHypRef Expression
1 wceq 1332 1 wff 𝑥 = 𝑦
 Colors of variables: wff set class Syntax hints:   = wceq 1332 This theorem is referenced by:  alequcoms  1497  equidqe  1513  ax4sp1  1514  equid  1679  nfequid  1680  stdpc6  1681  equcomi  1682  ax6evr  1683  equcom  1684  equcomd  1685  equcoms  1686  equtr  1687  equtrr  1688  equtr2  1689  equequ1  1690  equequ2  1691  elequ1  1692  elequ2  1693  ax11i  1694  ax10o  1695  ax10  1697  nfae  1699  hbaes  1700  hbnae  1701  nfnae  1702  hbnaes  1703  equsalh  1706  equsal  1707  dral1  1710  dral2  1711  drex2  1712  drnf1  1713  drnf2  1714  spimth  1715  spimh  1717  spimed  1720  cbv1  1724  cbv1h  1725  cbv2h  1726  cbvalh  1728  chvar  1732  sbimi  1739  sb1  1741  sb2  1742  sbequ1  1743  sbequ2  1744  sbequ12  1746  sbequ12r  1747  sbequ12a  1748  sbid  1749  stdpc4  1750  sbh  1751  sb6x  1754  sbequ5  1757  sbequ6  1758  equsb1  1760  equsb2  1761  sbiedh  1762  sbiedv  1764  sbieh  1765  equs5a  1768  drsb1  1773  exdistrfor  1774  sb4a  1775  equs45f  1776  sb6f  1777  sb5f  1778  sb4e  1779  hbsb2a  1780  hbsb2e  1781  sbcof2  1784  aev  1786  ax16  1787  dveeq2  1789  dveeq2or  1790  ax11v2  1794  ax11a2  1795  ax11b  1800  equs5  1803  equs5or  1804  sb3  1805  sb4  1806  sb4or  1807  sb4b  1808  sb4bor  1809  hbsb2  1810  nfsb2or  1811  sbequi  1813  sbequ  1814  drsb2  1815  spsbe  1816  spsbim  1817  sbequ8  1821  sbidm  1825  sb5rf  1826  sb6rf  1827  ax16i  1832  spv  1834  speiv  1836  equvin  1837  a16g  1838  a16gb  1839  a16nf  1840  sb56  1859  sb6  1860  sb5  1861  sbnv  1862  sbanv  1863  sborv  1864  sbi1v  1865  sbi2v  1866  cbval2  1895  cbvex2  1896  cbvaldva  1902  cbvexdva  1903  cbvex4v  1904  cleljust  1912  hbs1  1913  hbsbv  1916  nfsbxy  1917  nfsbxyt  1918  equsb3  1926  sbco  1943  sbcocom  1945  sbcomxyyz  1947  elsb3  1953  elsb4  1954  sb9v  1955  2sb5  1960  2sb6  1961  sbcom2v  1962  sb6a  1965  2sb5rf  1966  2sb6rf  1967  dfsb7  1968  sb7f  1969  sb7af  1970  sb10f  1972  sbel2x  1975  sbalyz  1976  sbal1yz  1978  sbal1  1979  sbexyz  1980  exsb  1985  2exsb  1986  dvelimALT  1987  dvelimfv  1988  hbsb4t  1990  nfsb4t  1991  dvelimf  1992  dvelimdf  1993  dvelimor  1995  dveeq1  1996  sbal2  1999  euf  2006  eubidh  2007  eubid  2008  hbeu1  2011  nfeu1  2012  sb8eu  2014  nfeuv  2019  sb8euh  2024  eu1  2026  mo2n  2029  euex  2031  eumo0  2032  mo23  2042  mor  2043  modc  2044  eu2  2045  eu3h  2046  mo2r  2053  mo3h  2054  mo2dc  2056  mo4f  2061  eu4  2063  moim  2065  moimv  2067  moanim  2075  mopick  2079  2eu4  2094  euequ1  2096  exists1  2097  axext3  2124  axext4  2125  bm1.1  2126  eleq1w  2202  cleqh  2241  cbvab  2265  sbab  2269  nfcjust  2271  drnfc1  2300  drnfc2  2301  dvelimdc  2303  dvelimc  2304  nfcvf  2305  cbvralf  2653  cbvrexf  2654  cbvreu  2657  cbvraldva2  2666  cbvrexdva2  2667  cbvraldva  2668  cbvrexdva  2669  cbvral2v  2670  cbvrex2v  2671  cbvral3v  2672  sbralie  2675  cbvrab  2689  vjust  2692  vex  2694  rr19.3v  2829  rr19.28v  2830  ralab2  2854  rexab2  2856  reu2  2878  reu6  2879  reu3  2880  rmo4  2883  reu4  2884  reu7  2885  reu8  2886  rmo3f  2887  rmo4f  2888  cdeqi  2900  cdeqri  2901  cdeqth  2902  cdeqnot  2903  cdeqal  2904  cdeqab  2905  cdeqim  2908  cdeqcv  2909  cdeqeq  2910  cdeqel  2911  nfccdeq  2913  sbsbc  2919  sbc8g  2922  sbcco2  2937  sbc5  2938  sbcralt  2991  sbcralg  2993  sbcreug  2995  rmo3  3006  cbvcsbw  3013  cbvcsb  3014  sbcel12g  3024  sbceqg  3025  cbvralcsf  3069  cbvrexcsf  3070  cbvreucsf  3071  cbvrabcsf  3072  difjust  3079  unjust  3081  injust  3083  dfss2f  3095  dfdif3  3193  dfnul3  3373  dfif3  3494  preq12bg  3710  eluniab  3758  elintab  3792  int0  3795  dfiunv2  3859  cbviun  3860  cbviin  3861  cbvdisj  3926  disjiun  3934  sndisj  3935  sbcbrg  3992  cbvmptf  4032  cbvmpt  4033  axsep2  4057  bm1.3ii  4059  nalset  4068  zfpow  4109  el  4112  dtruarb  4125  copsexg  4177  opelopabsb  4193  swopo  4239  pofun  4245  issod  4252  frind  4285  zfun  4367  ruv  4476  dtru  4486  dcextest  4506  tfisi  4512  findes  4528  relop  4701  dfdmf  4744  dfrnf  4792  resiexg  4876  dfres2  4883  opabresid  4884  mptresid  4885  imai  4907  issref  4933  intasym  4935  cnvi  4955  rnxpid  4985  cnvpom  5093  nfiota1  5102  cbviota  5105  sb8iota  5107  iotaval  5111  iotanul  5115  iota4  5118  csbiotag  5128  dffun2  5145  dffun4  5146  dffun5r  5147  dffun6f  5148  dffun4f  5151  sbcfung  5159  funopg  5169  funinsn  5184  funcnveq  5198  fun11  5202  fununi  5203  funcnvuni  5204  imain  5217  isarep2  5222  brprcneu  5426  fv2  5428  elfv  5431  fv3  5456  relelfvdm  5465  fvmpt2  5516  ralrnmpt  5574  rexrnmpt  5575  ffnfvf  5591  f1veqaeq  5682  dff13f  5683  fliftfuns  5711  cbvriota  5752  csbriotag  5754  acexmid  5785  oprabidlem  5814  cbvmpox  5861  cbvmpo  5862  cbvmpov  5863  mpofun  5885  abrexex2  6034  fmpoco  6125  f1o2ndf1  6137  poxp  6141  tposoprab  6189  tfrlem3-2d  6221  tfrlemi1  6241  tfr1onlemsucfn  6249  tfr1onlemaccex  6257  tfrcllemsucfn  6262  tfrcllemsucaccv  6263  tfrcllembxssdm  6265  tfrcllembfn  6266  tfrcllemaccex  6270  dcdifsnid  6412  fnsnsplitdc  6413  funresdfunsndc  6414  eqerlem  6472  qliftfuns  6525  eroveu  6532  cbvixp  6621  mptelixpg  6640  idssen  6683  xpf1o  6750  xpmapen  6756  findcard2d  6797  nnwetri  6821  fiintim  6834  snexxph  6855  fidcenumlemim  6857  fidcenumlemrk  6859  fidcenum  6861  supmoti  6897  isoti  6911  supisoti  6914  cnvti  6923  ordiso2  6937  ctssdccl  7013  finct  7018  infnninf  7023  onntri13  7118  onntri51  7119  onntri52  7122  cc1  7126  cc2  7128  ltsopi  7181  addpipqqs  7231  mulpipqqs  7234  archpr  7504  cauappcvgprlemlol  7508  cauappcvgprlemopu  7509  cauappcvgprlemupu  7510  cauappcvgprlemdisj  7512  cauappcvgprlemladdru  7517  cauappcvgprlemladdrl  7518  cauappcvgprlemlim  7522  caucvgprlemlol  7531  caucvgprlemopu  7532  caucvgprlemupu  7533  caucvgprlemdisj  7535  caucvgprlemloc  7536  caucvgprlemcl  7537  caucvgprlemladdrl  7539  caucvgprprlemcbv  7548  caucvgprprlemopu  7560  caucvgprprlemclphr  7566  caucvgprprlemexbt  7567  suplocexprlemmu  7579  suplocexprlemdisj  7581  caucvgsrlembound  7655  caucvgsrlembnd  7662  suplocsrlem  7669  suplocsr  7670  peano1nnnn  7713  axcaucvglemres  7760  axpre-suploc  7763  negf1o  8197  lbreu  8756  lbinf  8759  suprubex  8762  suprlubex  8763  suprleubex  8765  1nn  8784  uzind4s  9441  uzind4s2  9442  indstr  9444  supinfneg  9446  infsupneg  9447  eqreznegel  9462  lbzbi  9464  elpq  9496  exbtwnzlemex  10087  exbtwnz  10088  rebtwn2zlemstep  10090  rebtwn2z  10092  iseqovex  10289  iseqvalcbv  10290  seqvalcd  10292  seqovcd  10296  seq3f1olemqsum  10333  seq3f1olemp  10335  seq3f1oleml  10336  seq3distr  10346  faclbnd6  10551  fimaxq  10634  cvg1nlemres  10818  resqrexlemsqa  10857  resqrexlemex  10858  cau3lem  10947  fclim  11124  climeu  11126  cn1lem  11144  climcau  11177  climcvg1n  11180  summodclem3  11210  summodclem2a  11211  summodclem2  11212  summodc  11213  zsumdc  11214  fsum3  11217  isumz  11219  isumss2  11223  fsumsersdc  11225  fsum3ser  11227  fsumadd  11236  fsum2dlemstep  11264  fisumcom2  11268  isumshft  11320  cvgratz  11362  mertensabs  11367  prodfdivap  11377  cbvprod  11388  prodmodclem3  11405  prodmodclem2a  11406  prodmodclem2  11407  prodmodc  11408  zproddc  11409  fprodseq  11413  odd2np1lem  11641  zsupcl  11712  infssuzex  11714  infssuzledc  11715  bezoutlemmain  11758  bezoutlemeu  11767  gcdmultiple  11780  rplpwr  11787  pw2dvdseu  11918  hashdvds  11969  ennnfonelemg  11988  ennnfoneleminc  11996  ennnfonelemkh  11997  ennnfonelemhf1o  11998  ennnfonelemex  11999  ennnfonelemhom  12000  ennnfonelemrnh  12001  ennnfonelemfun  12002  ennnfonelemdm  12005  ennnfonelemr  12008  ennnfone  12010  inffinp1  12014  ctinf  12015  strsetsid  12067  baspartn  12292  cnpnei  12463  txdis1cn  12522  cnmptid  12525  xmetxp  12751  cncfmptc  12826  cncfmptid  12827  dedekindeulemloc  12841  dedekindicclemloc  12850  ivthinclemlr  12859  ivthinclemur  12861  ivthinclemloc  12863  ivthdec  12866  spimd  13182  2spim  13183  ch2var  13184  bj-sbimedh  13188  bj-sbimeh  13189  cbvrald  13205  sumdc2  13216  bdth  13245  bdcdeq  13253  bdne  13267  bdreu  13269  bdcsn  13284  bdsep2  13300  bdsepnft  13301  bdsepnfALT  13303  bdbm1.3ii  13305  bj-nalset  13309  bj-zfpair2  13324  bj-bdfindes  13363  bj-nn0suc0  13364  bj-nntrans  13365  setindft  13379  setindis  13381  bdsetindis  13383  bj-inf2vnlem3  13386  bj-inf2vnlem4  13387  strcoll2  13397  strcollnft  13398  strcollnfALT  13400  sscoll2  13402  nnti  13406  nnsf  13418  peano4nninf  13419  nninfsellemqall  13430  nninfomni  13434  trilpolemeq1  13454  tridceq  13470  redc0  13471  reap0  13472  dceqnconst  13473  dcapnconst  13474  nconstwlpolemgt0  13477
 Copyright terms: Public domain W3C validator