Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as." Instead, we will later use the biconditional connective for this purpose (df-or 224 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. Of course, we cannot use this mechanism to define the biconditional itself, since it hasn't been introduced yet.

In its most general form, a definition is simply an assertion that introduces a new symbol (or a new combination of existing symbols, as in df-3an 775) that is eliminable and does not strengthen the existing language. The latter requirement means that the set of provable statements not containing the new symbol (or new combination) should remain exactly the same after the definition is introduced. Our definition of the biconditional may look unusual compared to most definitions, but it strictly satisfies these requirements.

The justification for our definition is that if we mechanically replace the first wff above (the definiendum i.e. the thing being defined) with the second (the definiens i.e. the defining expression) in the definition, the definition becomes a substitution instance of previously proved theorem bijust 145. It is impossible to use df-bi 147 to prove any statement expressed in the original language that can't be proved from the original axioms. For if it were, we could replace it with instances of bijust 145 throughout the proof, thus obtaining a proof from the original axioms (contradiction).

Note that from Metamath's point of view, a definition is just another axiom - i.e. an assertion we claim to be true - but from our high level point of view, we are are not strengthening the language. To indicate this fact, we prefix definition labels with "df-" instead of "ax-". (This prefixing is an informal convention that means nothing to the Metamath proof verifier; it is just for human readability.)

See bii 158 and bi 513 for theorems suggesting the typical textbook definition of , showing that our definition has the properties we expect.