Users' Mathboxes Users' Mathboxes < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mathbox Unicode version

Theorem mathbox 23807
Description: (This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.)

A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of

For contributors:

By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of

Mathboxes are provided to help keep your work synchronized with changes in, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of that works with it.


1. If at all possible, please use only 0-ary class constants for new definitions, for example as in df-div 9624.

2. Try to follow the style of the rest of Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website.

3. Before submitting a revised mathbox, please make sure it verifies against the current

4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified that has mathboxes removed.


1. I may decide to move some theorems to the main part of for general use. In that case, an author acknowledgment will be added to the description of the theorem.

2. I may make changes to mathboxes to maintain the overall quality of Normally I will let you know if a change might impact what you are working on.

3. If you use theorems from another user's mathbox, I don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let me know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

Ref Expression
mathbox  |-  x  =  x

Proof of Theorem mathbox
StepHypRef Expression
1 equid 1684 1  |-  x  =  x
Colors of variables: wff set class
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator