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  cprodeq2ii  24135  cbvcprod  24137  prodrblem  24152  fprodcvg  24153  prodmolem3  24156  prodmolem2a  24157  prodmolem2  24158  prodmo  24159  zprod  24160  fprod  24164  fprodf1o  24172  eldm3  24190  fundmpss  24193  fununiq  24197  dfdm5  24203  dfrn5  24204  dfon2lem6  24215  dfon2  24219  rdgprc  24222  axextdfeq  24225  ax13dfeq  24226  cbvsetlike  24252  preddowncl  24267  poseq  24324  soseq  24325  wfrlem1  24327  wfrlem10  24336  wfr2  24344  frrlem1  24352  nodenselem5  24410  nocvxminlem  24415  nocvxmin  24416  nobndlem6  24422  nobndup  24425  nobnddown  24426  nofulllem4  24430  nofulllem5  24431  idsset  24501  dfbigcup2  24510  dffix2  24516  dffun10  24524  elfuns  24525  fnsingle  24529  dfiota3  24533  funimage  24538  fnimage  24539  brimg  24547  funpartfun  24553  brbtwn2  24605  colinearalg  24610  axsegconlem1  24617  axsegconlem10  24626  axlowdimlem15  24656  axeuclidlem  24662  axcontlem10  24673  segconeu  24706  btwndiff  24722  funtransport  24726  btwnconn1lem12  24793  btwnconn1lem14  24795  segleantisym  24810  outsideofeu  24826  funray  24835  funline  24837  hilbert1.2  24850  lineintmo  24852  onsuct0  24952  supaddc  24995  supadd  24996  ovoliunnfl  25001  ex-ovoliunnfl  25002  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  itgaddnclem2  25010  itgabsnc  25020  bddiblnc  25021  itggt0cn  25023  ftc1cnnclem  25024  ftc1cnnc  25025  areacirclem6  25033  areacirc  25034  axlll2  25131  srefwref  25170  celsor  25214  domintrefc  25228  mxlelt2  25368  ismxl2  25370  ismnl2  25371  mnlmxl2  25372  inposet  25381  mgmlion  25440  ltrooo  25507  cmprltr2  25514  glmrngo  25585  usptop  25653  fgsb2  25658  dfiunv2  26019  clscnc  26113  isconcl5ab  26205  bosser  26270  ismrcd2  26877  ismrc  26879  incssnn0  26889  nacsfix  26890  eldioph3  26948  eldioph4i  26998  fphpdo  27003  irrapxlem6  27015  pell1234qrreccl  27042  pell1234qrdich  27049  pell14qrexpclnn0  27054  rmxyval  27103  monotoddzzfi  27130  2nn0ind  27133  zindbi  27134  expmordi  27135  rmxypos  27137  jm2.17a  27150  jm2.17b  27151  rmygeid  27154  mzpcong  27162  acongrep  27170  jm2.18  27184  jm2.19lem3  27187  jm2.25  27195  jm2.26  27198  jm2.15nn0  27199  jm2.16nn0  27200  dford3lem2  27223  dnnumch1  27244  dnnumch3lem  27246  fnwe2lem2  27251  fnwe2lem3  27252  fnwe2  27253  aomclem3  27256  aomclem4  27257  kelac1  27264  kelac2lem  27265  filnm  27295  pwslnm  27299  uvcfval  27336  uvcval  27337  frlmsslsp  27351  lindff1  27393  hbtlem2  27431  hbtlem5  27435  hbt  27437  dgraalem  27453  mpaaeu  27458  matrng  27583  idomsubgmo  27617  expgrowth  27655  pm13.192  27713  pm13.193  27714  2sbc6g  27718  2sbc5g  27719  pm14.12  27724  pm14.122b  27726  pm14.24  27735  ipo0  27755  rexsb  28049  rexrsb  28050  2rexsb  28051  2rexrsb  28052  cbvral2  28053  cbvrex2  28054  rmoanim  28060  2reu4a  28070  2reu4  28071  sbcfun  28090  csbafv12g  28105  rlimdmafv  28145  csbaovg  28148  f1veqaeq  28188  opabex3d  28190  mpt2xopoveq  28201  injresinjlem  28214  injresinj  28215  hashgt12el  28218  usgraexmpl  28267  nbgranself  28283  nbcusgra  28298  uvtxnbgra  28306  cusgrauvtx  28309  wlkntrllem5  28349  wlkdvspthlem  28365  fargshiftf1  28382  constr3trllem2  28397  frgra3vlem1  28424  frgra3vlem2  28425  3vfriswmgralem  28428  3cyclfrgrarn1  28435  4cycl2vnunb  28439  n4cyclfrgra  28440  sb5ALT  28587  sbcoreleleq  28597  tratrb  28598  ordelordALT  28600  2pm13.193  28617  a9e2eq  28622  a9e2nd  28623  2uasbanh  28626  tratrbVD  28953  bnj23  29060  bnj1468  29194  bnj110  29206  bnj154  29226  bnj155  29227  bnj591  29259  bnj580  29261  bnj607  29264  bnj609  29265  bnj873  29272  bnj849  29273  bnj893  29276  bnj1123  29332  bnj1373  29376  bnj1388  29379  bnj1417  29387  bnj1489  29402  cbv3hvNEW7  29423  dvelimhwNEW7  29432  ax12olem2wAUX7  29433  ax12olem4wAUX7  29435  ax12olem6NEW7  29436  dvelimvNEW7  29439  dveeq2NEW7  29440  dveeq1NEW7  29441  ax9NEW7  29445  ax9oNEW7  29446  a9eNEW7  29447  ax10lem4NEW7  29448  ax10lem5NEW7  29449  ax10NEW7  29450  aecomsNEW7  29452  ax10oNEW7  29453  hba1eAUX7  29454  hbaewAUX7  29455  hbaew2AUX7  29456  nfaewAUX7  29457  hbnaewAUX7  29458  nfnaewAUX7  29459  nfaew2AUX7  29460  hbnaew2AUX7  29461  nfnaew2AUX7  29462  nfeqfNEW7  29463  equsalNEW7  29464  equsalihAUX7  29465  equsexNEW7  29467  dvelimhvAUX7  29469  dral1NEW7  29470  drex1NEW7  29471  drnf1NEW7  29472  dral2wAUX7  29473  drex2wAUX7  29474  drnf2wAUX7  29475  dral2w2AUX7  29476  drex2w2AUX7  29477  drnf2w2AUX7  29478  dral2w3AUX7  29479  drex2w3AUX7  29480  drnf2w3AUX7  29481  exdistrfNEW7  29482  drsb1NEW7  29483  spimtNEW7  29484  spimNEW7  29485  spimeNEW7  29486  spimedNEW7  29487  cbv1hwAUX7  29488  cbv2hwAUX7  29490  cbv3wAUX7  29492  cbv3hwAUX7  29493  cbvalwwAUX7  29494  cbvexwAUX7  29495  aevwAUX7  29497  aevNEW7  29498  hbaew3AUX7  29499  nfaew3AUX7  29500  nfnaew3AUX7  29501  equviniNEW7  29502  equveliNEW7  29503  equvinNEW7  29504  ax11v2NEW7  29505  ax11a2NEW7  29506  equs4NEW7  29508  equs5NEW7  29509  equs5bAUX7  29510  ax15NEW7  29511  sb2NEW7  29512  equsb1NEW7  29513  equsb2NEW7  29514  sbiedNEW7  29515  sbieNEW7  29516  hbsb2aNEW7  29517  hbsb2eNEW7  29518  a16gNEW7  29521  a16gbNEW7  29522  a16nfwAUX7  29523  a16nfNEW7  29525  ax16iNEW7  29526  sb4NEW7  29527  sb4bNEW7  29528  hbsb2NEW7  29529  stdpc4NEW7  29530  sbftNEW7  29531  sbequ5wAUX7  29533  nfsb2NEW7  29536  sbnNEW7  29537  sbi1NEW7  29538  sbequ8NEW7  29550  nfsb4twAUX7  29551  nfsb4wAUX7  29552  sbequiNEW7  29553  sbequNEW7  29554  drsb2NEW7  29555  sbcoNEW7  29556  sbidmNEW7  29558  sbco2wAUX7  29559  sbco3wAUX7  29561  sbcomwAUX7  29562  sb5rfNEW7  29563  sb6rfNEW7  29564  ax11vNEW7  29567  sb56NEW7  29568  sb6NEW7  29569  sb5NEW7  29570  exsbNEW7  29571  equsb3lemNEW7  29573  equsb3NEW7  29574  hbs1NEW7  29577  2sb5NEW7  29581  2sb6NEW7  29582  sb6aNEW7  29583  sbelxNEW7  29585  sbel2xNEW7  29586  sbal1NEW7  29587  sbalNEW7  29588  naecomsNEW7  29591  chvarNEW7  29592  equs45fNEW7  29593  ax11bNEW7  29594  spvNEW7  29595  speivNEW7  29597  cleljustNEW7  29599  cleljustALTNEW7  29600  sb6xNEW7  29601  sbiedvNEW7  29604  sb6fNEW7  29605  sb5fNEW7  29606  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