Theorem sandbox 8636

Description: (This theorem is a dummy placeholder for these guidelines.)

"Sandboxes" are user-contributed sections that are not officially part of set.mm. They are included in the set.mm file in order to ensure that they are kept synchronized with label, definition, and theorem changes in set.mm. Eventually they may be broken out as separate modules, particularly in conjunction with any future Ghilbert translation.

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

Sandboxes are provided as a courtesy to keep your work synchronized, 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.

Notes:

1. I (N. Megill) have not necessarily checked definitions for soundness nor for agreement with the literature. In particular, a proof that 1 = 0 based on a sandbox definition will not considered in any challenge to prove set.mm inconsistent. (Such a proof will still be welcome, of course, so that the erroneous definition can be corrected.)

2. Over time I may decide to make a theorem "official," in which case it will be moved to the appropriate section of set.mm with an author acknowledgment.

3. At any time, I may revise definitions, theorems, proofs, and statement descriptions; add or delete theorems and/or definitions; or delete part or all of a sandbox if I feel it will not ultimately be useful or for any other reason.

Guidelines:

1. If at all possible, please use only 0-ary class constants for new definitions, to make soundness checking easier.

2. Please 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 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.

Assertion

Ref	Expression
sandbox	|- x = x

Proof of Theorem sandbox

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

Syntax hints:   = wceq 1099

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957

Copyright terms: Public domain