Theorem mathbox 11806

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 set.mm.

For contributors:

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

Mathboxes are provided to help keep your work synchronized with changes in set.mm, 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 set.mm that works with it.

Guidelines:

1. If at all possible, please use only 0-ary class constants for new definitions.

2. Try to follow the style of the rest of set.mm in terms of indentation, line length (79 characters or less), and comment markup (see "Auxiliary keywords" under HELP LANGUAGE in metamath.exe). Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. All mathbox content will be on public display and should hopefully reflect the overall quality of the web site.

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

4. Mathboxes should be independent. To verify this, verify your mathbox with all other mathboxes removed. If you need a theorem from another mathbox, let me know so I can move the theorem to the main section. Please do not run 'minimize' against theorems in other mathboxes.

Notes:

1. I may decide to move some theorems to the main part of set.mm 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 set.mm. 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.)

Assertion

Ref	Expression
mathbox	|- x = x

Proof of Theorem mathbox

Step	Hyp	Ref	Expression
1		equid 1322	1 |- x = x

Syntax hints:   = wceq 1136

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1143  ax-12 1148  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319

Copyright terms: Public domain