MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  weq Unicode version

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

(Instead of introducing weq 1633 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 1632. This lets us avoid overloading the  = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1633 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1632. 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
StepHypRef Expression
1 wceq 1632 1  wff  x  =  y
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  equs3  1634  speimfw  1635  spimfw  1636  ax11i  1637  sbequ2  1640  sb1  1641  sbimi  1642  a9ev  1646  exiftru  1647  spimw  1656  spnfw  1658  equid  1662  nfequid  1663  equcomi  1664  equcom  1665  equcoms  1666  equequ1  1667  equequ1OLD  1668  equequ2  1669  stdpc6  1670  equtr  1671  equtrr  1672  equtr2  1673  ax12b  1674  ax12bOLD  1675  spfw  1676  spnfwOLD  1677  spw  1679  spvwOLD  1680  spfalw  1685  19.2OLD  1686  cbvalw  1687  cbvalvw  1688  cbvexvw  1689  alcomiw  1690  hba1w  1693  hbe1w  1694  elequ1  1699  elequ2  1701  ax9dgen  1702  ax11w  1707  ax11dgen  1708  ax11wdemo  1709  ax12w  1710  ax12dgen1  1711  ax12dgen2  1712  ax12dgen3  1713  sp  1728  spimeh  1734  equsalhw  1742  dvelimhw  1747  cbv3hv  1749  equs5a  1840  equs5e  1841  sbequ1  1871  sbequ12  1872  sbequ12r  1873  sbequ12a  1874  sbid  1875  sb4a  1876  sb4e  1877  ax12olem1  1880  ax12olem2  1881  ax12olem3  1882  ax12olem4  1883  ax12olem5  1884  ax12olem6  1885  ax12  1888  ax10lem1  1889  ax10lem2  1890  ax10lem3  1891  dvelimv  1892  dveeq2  1893  ax10lem4  1894  ax10lem5  1895  ax10lem6  1896  ax10  1897  a16g  1898  aecoms  1900  naecoms  1901  ax9  1902  ax9o  1903  a9e  1904  ax10o  1905  hbae  1906  nfae  1907  hbnae  1908  nfnae  1909  hbnaes  1910  nfeqf  1911  equs4  1912  equsal  1913  equsex  1915  dvelimh  1917  dral1  1918  dral2  1919  drex1  1920  drex2  1921  drnf1  1922  drnf2  1923  exdistrf  1924  nfald2  1925  nfexd2  1926  spimt  1927  spim  1928  spime  1929  spimed  1930  cbv1h  1931  cbv2h  1933  cbv3  1935  cbv3h  1936  cbval  1937  cbvex  1938  chvar  1939  equvini  1940  equveli  1941  equs45f  1942  aev  1944  ax11v2  1945  ax11a2  1946  ax11b  1948  equs5  1949  dvelimf  1950  spv  1951  speiv  1953  equvin  1954  cbval2  1957  cbvex2  1958  cbvexd  1962  cbvaldva  1963  cbvexdva  1964  cbvex4v  1965  cleljust  1967  cleljustALT  1968  dveeq1  1971  ax15  1974  drsb1  1975  sb2  1976  stdpc4  1977  sbft  1978  sb6x  1982  sbequ5  1984  sbequ6  1985  equsb1  1987  equsb2  1988  sbied  1989  sbiedv  1990  sbie  1991  sb6f  1992  sb5f  1993  hbsb2a  1994  hbsb2e  1995  ax16i  1999  ax16ALT2  2001  a16gALT  2002  a16gb  2003  a16nf  2004  sb3  2005  sb4  2006  sb4b  2007  dfsb2  2008  dfsb3  2009  hbsb2  2010  nfsb2  2011  sbequi  2012  sbequ  2013  drsb2  2014  sbn  2015  sbi1  2016  sbequ8  2032  nfsb4t  2033  nfsb4  2034  dvelimdf  2035  sbco  2036  sbidm  2038  sbco2  2039  sbco3  2041  sbcom  2042  sb5rf  2043  sb6rf  2044  sb9i  2047  ax11v  2049  sb56  2050  sb6  2051  sb5  2052  equsb3lem  2053  equsb3  2054  hbs1  2057  nfsb  2061  nfsbd  2063  2sb5  2064  2sb6  2065  sbcom2  2066  pm11.07  2067  sb6a  2068  2sb5rf  2069  2sb6rf  2070  dfsb7  2071  sb7f  2072  sb10f  2074  sbelx  2076  sbel2x  2077  sbal1  2078  sbal  2079  exsb  2082  2exsb  2084  dvelimALT  2085  sbal2  2086  ax9from9o  2100  aecom-o  2103  aecoms-o  2104  hbae-o  2105  dral1-o  2106  ax11  2107  ax12from12o  2108  equid1  2110  hbequid  2112  nfequid-o  2113  equidqe  2125  ax4sp1  2126  equidq  2127  equid1ALT  2128  ax10from10o  2129  naecoms-o  2130  hbnae-o  2131  dvelimf-o  2132  dral2-o  2133  aev-o  2134  ax17eq  2135  dveeq2-o  2136  dveeq2-o16  2137  a16g-o  2138  dveeq1-o  2139  dveeq1-o16  2140  ax17el  2141  ax10-16  2142  ax11f  2144  ax11eq  2145  ax11el  2146  ax11indn  2147  ax11indi  2148  ax11indalem  2149  ax11inda2ALT  2150  ax11inda2  2151  ax11inda  2152  ax11v2-o  2153  ax11a2-o  2154  ax10o-o  2155  eujustALT  2159  eumo0  2180  eu2  2181  eu3  2182  mo2  2185  mo3  2187  mo4f  2188  eu4  2195  moanim  2212  2eu5  2240  euequ1  2244  cleqh  2393  nfrmod  2726  nfrmo  2728  cbvraldva2  2781  cbvrexdva2  2782  cbvraldva  2783  cbvrexdva  2784  cbvrex2v  2786  rmo4  2971  reu4  2972  2reu5lem3  2985  2reu5  2986  sbsbc  3008  sbc8g  3011  sbc2or  3012  sbcco2  3027  sbc5  3028  sbcralt  3076  sbcralg  3078  sbcrexg  3079  sbcreug  3080  rmo2  3089  rmo2i  3090  rmo3  3091  sbcel12g  3109  sbceqg  3110  cbvralcsf  3156  cbvrabcsf  3159  csbifg  3606  preq12bg  3807  cbvdisj  4019  nfdisj  4021  disjor  4023  disjiun  4029  sbcbrg  4088  opelopabsb  4291  somo  4364  wereu2  4406  onminex  4614  tfindes  4669  tfinds2  4670  findes  4702  opabresid  5019  mptresid  5020  issref  5072  iota4  5253  csbiotag  5264  brprcneu  5534  fv2  5536  ralrnmpt  5685  foeqcnvco  5820  soisoi  5841  isosolem  5860  mpt2fun  5962  poxp  6243  sorpss  6298  sorpssuni  6302  sorpssint  6303  sorpsscmpl  6304  csbriotag  6333  smo11  6397  smogt  6400  seqomlem0  6477  omeulem1  6596  nnawordi  6635  eqerlem  6708  ixpsnf1o  6872  boxriin  6874  infensuc  7055  unxpdomlem1  7083  findcard2  7114  ac6sfi  7117  indexfi  7179  supmo  7219  wemaplem1  7277  r111  7463  scottexs  7573  scott0s  7574  cardprc  7629  alephf1  7728  alephle  7731  ackbij1lem14  7875  ackbij1lem16  7877  ackbij1lem17  7878  ackbij2lem3  7883  ackbij2lem4  7884  sornom  7919  fin23lem26  7967  fin23lem14  7975  fin23lem15  7976  fin1a2lem2  8043  fin1a2lem4  8045  itunitc1  8062  ituniiun  8064  domtriom  8085  axdc2  8091  axdc3lem3  8094  axac3  8106  axac2  8109  axac  8110  axdc  8164  brdom7disj  8172  konigth  8207  fpwwe2cbv  8268  grothomex  8467  uzind4s  10294  uzind4s2  10295  rpnnen1lem4  10361  facwordi  11318  faclbnd6  11328  wrdind  11493  sqrmo  11753  rexfiuz  11847  odd2np1lem  12602  bezoutlem4  12736  bezout  12737  gcdmultiple  12745  rplpwr  12751  prmind2  12785  isprm5  12807  prmpwdvds  12967  mreexexlemd  13562  isacs2  13571  isacs1i  13575  mreacs  13576  acsfn  13577  catideu  13593  ispos2  14098  posprs  14099  isposd  14105  pospropd  14254  odupos  14255  poslubmo  14266  ipopos  14279  ipodrsima  14284  latdisdlem  14308  latdisd  14309  spwmo  14351  mgmidmo  14386  prdsinvlem  14619  lssats2  15773  lspextmo  15829  lspsneq  15891  lspsneu  15892  ply1sclf1  16380  baspartn  16708  neindisj2  16876  2ndcdisj  17198  qtophmeo  17524  elmptrab  17538  isfildlem  17568  fgcl  17589  evlseu  19416  ply1divmo  19537  ig1peu  19573  aaliou3lem5  19743  aaliou3lem6  19744  aaliou3lem7  19745  aaliou3  19747  avril1  20852  isgrpo2  20880  cdjreui  23028  cvmliftmo  23830  cvmlift2lem13  23861  cvmlift3  23874  axextprim  24062  axrepprim  24063  axpowprim  24065  axacprim  24068  untangtr  24075  dfso3  24089  faclimlem3  24119  faclimlem5  24121  faclim  24126  prodeq2ii  24135  cbvcprod  24137  prodrblem  24152  fprodcvg  24153  prodmolem3  24156  prodmolem2a  24157  prodmolem2  24158  prodmo  24159  zprod  24160  fprod  24164  fprodf1o  24171  eldm3  24189  fundmpss  24192  fununiq  24196  dfdm5  24202  dfrn5  24203  dfon2lem6  24214  dfon2  24218  rdgprc  24221  axextdfeq  24224  ax13dfeq  24225  cbvsetlike  24251  preddowncl  24266  poseq  24323  soseq  24324  wfrlem1  24326  wfrlem10  24335  wfr2  24343  frrlem1  24351  nodenselem5  24409  nocvxminlem  24414  nocvxmin  24415  nobndlem6  24421  nobndup  24424  nobnddown  24425  nofulllem4  24429  nofulllem5  24430  idsset  24500  dfbigcup2  24509  dffix2  24515  dffun10  24523  elfuns  24524  fnsingle  24528  dfiota3  24532  funimage  24537  fnimage  24538  brimg  24546  funpartfun  24552  brbtwn2  24604  colinearalg  24609  axsegconlem1  24616  axsegconlem10  24625  axlowdimlem15  24655  axeuclidlem  24661  axcontlem10  24672  segconeu  24705  btwndiff  24721  funtransport  24725  btwnconn1lem12  24792  btwnconn1lem14  24794  segleantisym  24809  outsideofeu  24825  funray  24834  funline  24836  hilbert1.2  24849  lineintmo  24851  onsuct0  24951  supaddc  24994  supadd  24995  ovoliunnfl  25000  ex-ovoliunnfl  25001  itg2addnclem  25002  itg2addnc  25004  itg2gt0cn  25005  itgaddnclem2  25009  itgabsnc  25019  bddiblnc  25020  itggt0cn  25022  ftc1cnnclem  25023  ftc1cnnc  25024  areacirclem6  25032  areacirc  25033  axlll2  25130  srefwref  25169  celsor  25213  domintrefc  25227  mxlelt2  25367  ismxl2  25369  ismnl2  25370  mnlmxl2  25371  inposet  25380  mgmlion  25439  ltrooo  25506  cmprltr2  25513  glmrngo  25584  usptop  25652  fgsb2  25657  dfiunv2  26018  clscnc  26112  isconcl5ab  26204  bosser  26269  ismrcd2  26876  ismrc  26878  incssnn0  26888  nacsfix  26889  eldioph3  26947  eldioph4i  26997  fphpdo  27002  irrapxlem6  27014  pell1234qrreccl  27041  pell1234qrdich  27048  pell14qrexpclnn0  27053  rmxyval  27102  monotoddzzfi  27129  2nn0ind  27132  zindbi  27133  expmordi  27134  rmxypos  27136  jm2.17a  27149  jm2.17b  27150  rmygeid  27153  mzpcong  27161  acongrep  27169  jm2.18  27183  jm2.19lem3  27186  jm2.25  27194  jm2.26  27197  jm2.15nn0  27198  jm2.16nn0  27199  dford3lem2  27222  dnnumch1  27243  dnnumch3lem  27245  fnwe2lem2  27250  fnwe2lem3  27251  fnwe2  27252  aomclem3  27255  aomclem4  27256  kelac1  27263  kelac2lem  27264  filnm  27294  pwslnm  27298  uvcfval  27335  uvcval  27336  frlmsslsp  27350  lindff1  27392  hbtlem2  27430  hbtlem5  27434  hbt  27436  dgraalem  27452  mpaaeu  27457  matrng  27582  idomsubgmo  27616  expgrowth  27654  pm13.192  27712  pm13.193  27713  2sbc6g  27717  2sbc5g  27718  pm14.12  27723  pm14.122b  27725  pm14.24  27734  ipo0  27754  rexsb  28048  rexrsb  28049  2rexsb  28050  2rexrsb  28051  cbvral2  28052  cbvrex2  28053  rmoanim  28059  2reu4a  28069  2reu4  28070  sbcfun  28089  csbafv12g  28104  rlimdmafv  28144  csbaovg  28147  f1veqaeq  28187  opabex3d  28189  mpt2xopoveq  28200  injresinjlem  28213  injresinj  28214  hashgt12el  28217  usgraexmpl  28266  nbgranself  28282  nbcusgra  28297  uvtxnbgra  28305  cusgrauvtx  28308  wlkntrllem5  28348  wlkdvspthlem  28364  fargshiftf1  28381  constr3trllem2  28396  frgra3vlem1  28423  frgra3vlem2  28424  3vfriswmgralem  28427  3cyclfrgrarn1  28434  4cycl2vnunb  28438  n4cyclfrgra  28439  sb5ALT  28586  sbcoreleleq  28596  tratrb  28597  ordelordALT  28599  2pm13.193  28616  a9e2eq  28621  a9e2nd  28622  2uasbanh  28625  tratrbVD  28952  bnj23  29059  bnj1468  29193  bnj110  29205  bnj154  29225  bnj155  29226  bnj591  29258  bnj580  29260  bnj607  29263  bnj609  29264  bnj873  29271  bnj849  29272  bnj893  29275  bnj1123  29331  bnj1373  29375  bnj1388  29378  bnj1417  29386  bnj1489  29401  cbv3hvNEW7  29422  dvelimhwNEW7  29431  ax12olem2wAUX7  29432  ax12olem4wAUX7  29434  ax12olem6NEW7  29435  dvelimvNEW7  29438  dveeq2NEW7  29439  dveeq1NEW7  29440  ax9NEW7  29444  ax9oNEW7  29445  a9eNEW7  29446  ax10lem4NEW7  29447  ax10lem5NEW7  29448  ax10NEW7  29449  aecomsNEW7  29451  ax10oNEW7  29452  hba1eAUX7  29453  hbaewAUX7  29454  hbaew2AUX7  29455  nfaewAUX7  29456  hbnaewAUX7  29457  nfnaewAUX7  29458  nfaew2AUX7  29459  hbnaew2AUX7  29460  nfnaew2AUX7  29461  nfeqfNEW7  29462  equsalNEW7  29463  equsalihAUX7  29464  equsexNEW7  29466  dvelimhvAUX7  29468  dral1NEW7  29469  drex1NEW7  29470  drnf1NEW7  29471  dral2wAUX7  29472  drex2wAUX7  29473  drnf2wAUX7  29474  dral2w2AUX7  29475  drex2w2AUX7  29476  drnf2w2AUX7  29477  dral2w3AUX7  29478  drex2w3AUX7  29479  drnf2w3AUX7  29480  exdistrfNEW7  29481  drsb1NEW7  29482  spimtNEW7  29483  spimNEW7  29484  spimeNEW7  29485  spimedNEW7  29486  cbv1hwAUX7  29487  cbv2hwAUX7  29489  cbv3wAUX7  29491  cbv3hwAUX7  29492  cbvalwwAUX7  29493  cbvexwAUX7  29494  aevwAUX7  29496  aevNEW7  29497  hbaew3AUX7  29498  nfaew3AUX7  29499  nfnaew3AUX7  29500  equviniNEW7  29501  equveliNEW7  29502  equvinNEW7  29503  ax11v2NEW7  29504  ax11a2NEW7  29505  equs4NEW7  29507  equs5NEW7  29508  equs5bAUX7  29509  ax15NEW7  29510  sb2NEW7  29511  equsb1NEW7  29512  equsb2NEW7  29513  sbiedNEW7  29514  sbieNEW7  29515  hbsb2aNEW7  29516  hbsb2eNEW7  29517  a16gNEW7  29520  a16gbNEW7  29521  a16nfwAUX7  29522  a16nfNEW7  29524  ax16iNEW7  29525  sb4NEW7  29526  sb4bNEW7  29527  hbsb2NEW7  29528  stdpc4NEW7  29529  sbftNEW7  29530  sbequ5wAUX7  29532  nfsb2NEW7  29535  sbnNEW7  29536  sbi1NEW7  29537  sbequ8NEW7  29549  nfsb4twAUX7  29550  nfsb4wAUX7  29551  sbequiNEW7  29552  sbequNEW7  29553  drsb2NEW7  29554  sbcoNEW7  29555  sbidmNEW7  29557  sbco2wAUX7  29558  sbco3wAUX7  29560  sbcomwAUX7  29561  sb5rfNEW7  29562  sb6rfNEW7  29563  ax11vNEW7  29566  sb56NEW7  29567  sb6NEW7  29568  sb5NEW7  29569  exsbNEW7  29570  equsb3lemNEW7  29572  equsb3NEW7  29573  hbs1NEW7  29576  2sb5NEW7  29580  2sb6NEW7  29581  sb6aNEW7  29582  sbelxNEW7  29584  sbel2xNEW7  29585  sbal1NEW7  29586  sbalNEW7  29587  naecomsNEW7  29590  chvarNEW7  29591  equs45fNEW7  29592  ax11bNEW7  29593  spvNEW7  29594  speivNEW7  29596  cleljustNEW7  29598  cleljustALTNEW7  29599  sb6xNEW7  29600  sbiedvNEW7  29603  sb6fNEW7  29604  sb5fNEW7  29605  dvelimALTNEW7  29607  sb3NEW7  29608  dfsb2NEW7  29609  dfsb3NEW7  29610  ax7w1AUX7  29615  ax7w1hAUX7  29616  hbaew0AUX7  29617  hbaew4AUX7  29618  hbaew5AUX7  29619  ax7w2AUX7  29620  ax7w3AUX7  29621  ax7w6AUX7  29622  ax7w7AUX7  29623  ax7w9AUX7  29630  alcomw9bAUX7  29631  ax12olem2OLD7  29660  ax12olem4OLD7  29661  hbaeOLD7  29662  nfaeOLD7  29663  hbnaeOLD7  29664  nfnaeOLD7  29665  hbnaesOLD7  29666  dvelimhOLD7  29667  dral2OLD7  29668  drex2OLD7  29669  drnf2OLD7  29670  nfald2OLD7  29671  nfexd2OLD7  29672  cbv1hOLD7  29673  cbv2hOLD7  29675  cbv3OLD7  29677  cbv3hOLD7  29678  cbvalOLD7  29679  cbvexOLD7  29680  dvelimfOLD7  29681  cbval2OLD7  29684  cbvex2OLD7  29685  cbvexdOLD7  29689  cbvaldvaOLD7  29690  cbvexdvaOLD7  29691  cbvex4vOLD7  29692  sbequ5OLD7  29695  sbequ6OLD7  29696  ax16ALT2OLD7  29697  a16gALTOLD7  29698  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  nfsb4OLD7  29701  nfsbOLD7  29702  nfsbdOLD7  29704  dvelimdfOLD7  29705  sbco2OLD7  29706  sbco3OLD7  29708  sbcomOLD7  29709  sb9iOLD7  29712  sbcom2OLD7  29715  pm11.07OLD7  29716  2sb5rfOLD7  29717  2sb6rfOLD7  29718  dfsb7OLD7  29719  sb7fOLD7  29720  sb10fOLD7  29722  2exsbOLD7  29723  sbal2OLD7  29724  ax12-2  29725  ax12-3  29726  ax12OLD  29727  ax12-4  29728  ax12conj2  29730  hbae-x12  29731  hbnae-x12  29732  a12stdy1-x12  29733  a12stdy2-x12  29734  equsexv-x12  29735  equvinv  29736  equveliv  29737  equvelv  29738  a12study4  29739  a12study6  29740  a12study8  29741  a12study9  29742  a12peros  29743  a12study5rev  29744  ax10lem17ALT  29745  ax10lem18ALT  29746  a12stdy1  29748  a12stdy2  29749  a12stdy3  29750  a12stdy4  29751  a12lem2  29753  a12studyALT  29755  a12study3  29757  a12study10  29758  a12study10n  29759  a12study11  29760  a12study11n  29761  ax9lem1  29762  ax9lem2  29763  ax9lem3  29764  ax9lem4  29765  ax9lem5  29766  ax9lem6  29767  ax9lem12  29773  ax9lem13  29774  ax9lem14  29775  ax9lem15  29776  ax9lem16  29777  ax9lem17  29778  ax9lem18  29779  ax9vax9  29780  lshpkrlem3  29924  lshpkrcl  29928  glbconN  30188  lplnexllnN  30375  pmapglb  30581  lnatexN  30590  paddasslem5  30635  paddasslem12  30642  paddasslem14  30644  polval2N  30717  pexmidlem1N  30781  trlord  31380  cdlemk28-3  31719  diaf11N  31861  dibf11N  31973  dihordlem7b  32027  dihord10  32035  dihlsscpre  32046  dihf11  32079  dihglblem2aN  32105  dihglblem2N  32106  dihmeetlem15N  32133  dihglb2  32154  dvh3dim2  32260  dochexmidlem1  32272  lcfl7N  32313  lclkrs2  32352  lcfrlem9  32362  lcf1o  32363  lcfrlem39  32393  lcfr  32397  mapdval4N  32444  mapdrvallem3  32458  mapdrval  32459  mapd1o  32460  mapd0  32477  mapdpglem30  32514  mapdpglem31  32515  mapdpglem32  32517  mapdpg  32518  mapdh9a  32602  mapdh9aOLDN  32603  hdmap1cbv  32615  hdmapf1oN  32680  hdmap14lem6  32688  hgmapf1oN  32718
  Copyright terms: Public domain W3C validator