`∈`

(is an element of) for set theory or `+`

(addition) for Peano arithmetic.
stmt (EqualityBuilder () () (→ (∧ (= s0 s1) (= t0 t1)) (↔ (= s0 t0) (= s1 t1))))
stmt (buildEquality () ((= s0 s1) (= t0 t1)) (↔ (= s0 t0) (= s1 t1)))
#
# We also supply a variety of variant builders, for convenience:
stmt (EqualityBuilderRR () () (→ (= s0 s1) (↔ (= s0 t) (= s1 t))))
stmt (buildEqualityRR () ((= s0 s1)) (↔ (= s0 t) (= s1 t)))
stmt (EqualityBuilderLL () () (→ (= s0 s1) (↔ (= t s0) (= t s1))))
stmt (buildEqualityLL () ((= t0 t1)) (↔ (= s t0) (= s t1)))
stmt (buildEqualityInConsequent ()
((→ φ (= s0 s1))
(→ φ (= t0 t1)))
(→ φ (↔ (= s0 t0) (= s1 t1))))
stmt (buildEqualityRRInConsequent ()
((→ φ (= s0 s1)))
(→ φ (↔ (= s0 t) (= s1 t))))
stmt (buildEqualityLLInConsequent ()
((→ φ (= t0 t1)))
(→ φ (↔ (= s t0) (= s t1))))
#
# To say that two terms are not equal, we simply use `(¬ (= s t))`

. Ghilbert then typesets that as `s ≠ t`

.
#
# == Free variables ==
# Metamath has `φ → ∀ x φ`

as a way to say that a variable is not free in a formula, but we rely instead on the free variable features built in to ghilbert.
# === Adding or removing quantifiers ===
# If a variable is not free in a formula, it is legitimate to add or remove quantifiers from that formula:
stmt (ForAllAddRemove ((φ x)) () (↔ (∀ x φ) φ))
stmt (ThereExistsAddRemove ((φ x)) () (↔ (∃ x φ) φ))
#
# === Moving formulas in and out of quantification ===
# The results in this section all have to do with being able to move around formulas relative to quantifiers, given that the quantified variable is not free in the formula being moved.
#
stmt (ForAllImplicationConsequentMovement ((ψ x)) () (↔ (∀ x (→ φ ψ)) (→ (∃ x φ) ψ)))
stmt (ThereExistsConjunctionMovement ((φ x)) () (↔ (∃ x (∧ φ ψ)) (∧ φ (∃ x ψ))))
stmt (ThereExistsConjunctionRightMovement ((ψ x)) () (↔ (∃ x (∧ φ ψ)) (∧ (∃ x φ) ψ)))
stmt (ThereExistsDisjunctionMovement ((φ x)) () (↔ (∃ x (∨ φ ψ)) (∨ φ (∃ x ψ))))
stmt (ThereExistsDisjunctionRightMovement ((ψ x)) () (↔ (∃ x (∨ φ ψ)) (∨ (∃ x φ) ψ)) )
stmt (ThereExistsAntecedentMovement ((φ x)) () (↔ (∃ x (→ φ ψ)) (→ φ (∃ x ψ))))
#
# Here are a few rules based on these:
stmt (moveLeftConjunctIntoThereExistsInConsequent ((φ x))
((→ antecedent (∧ φ (∃ x ψ))))
(→ antecedent (∃ x (∧ φ ψ))))
stmt (moveRightConjunctIntoThereExistsInConsequent ((ψ x))
((→ antecedent (∧ (∃ x φ) ψ)))
(→ antecedent (∃ x (∧ φ ψ))))
stmt (repeatAntecedentThereExists ((antecedent x))
((→ antecedent (∃ x ψ)))
(→ antecedent (∃ x (∧ antecedent ψ))))
#
# ==== Scattering and gathering ====
# If we have two formulas joined by a conjunction, one quantified over one variable and the other quantified over another, we can express the quantifiers either at the beginning or with the formulas they apply to.[http://us.metamath.org/mpeuni/eeanv.html eeanv], metamath's set.mm, accessed August 8, 2010 We name the propositions `φx`

and `ψy`

to express the idea that `φx`

will typically contain `x`

and `ψy`

will typically contain `y`

.
tvar (formula ψy)
stmt (ThereExistsScattering ((φx y) (ψy x)) ()
(↔ (∃ x (∃ y (∧ φx ψy))) (∧ (∃ x φx) (∃ y ψy))))
stmt (gatherThereExistsInConsequent ((φx y) (ψy x)) ((→ antecedent (∧ (∃ x φx) (∃ y ψy))))
(→ antecedent (∃ x (∃ y (∧ φx ψy)))))
#
# ==== Adding quantifiers to theorems which are implications ====
#
# These variants on moving formulas turn out to be used particularly often:
stmt (addThereExistsToAntecedent ((ψ x))
((→ φ ψ))
(→ (∃ x φ) ψ))
stmt (addForAllToConsequent ((φ x))
((→ φ ψ))
(→ φ (∀ x ψ)))
#
# == Converting variable to object ==
# We can convert a formula containing a variable `x`

to one containing an object `s`

using the following theorem.
stmt (VariableToObject ((s x) (φs x))
((→ (= x s) (↔ φx φs))
φx
)
φs)
#
# == Substitution ==
# Having a formula which substitutes one variable for another greatly increases the readability of many theorems. For example, a statement of [[w:mathematical induction|induction]] will generally apply the same formula with `0`

, `k`

, `k + 1`

, or `n`

.
#
# This kind of substitution is known as ''proper substitution'' as there are some rules about what kinds of substitution are valid. The following theorems enable making proper substitutions.
#
# We first define the `subst`

term:
#
term (formula (subst s x φ) (x s))
#
# so for example `(subst s x φ)`

can be thought of as a copy of `φ`

in which `x`

is changed to `s`

. In more conventional notation this would be `[s / x] φ`

(or, using a common but potentially ambiguous notation, changing `φ(x)`

to `φ(s)`

).
#
# === Building up expressions involving subst ===
#
# If we have a theorem, we can add a variable substitution onto it.
stmt (introduceSubst () (φ) (subst s x φ))
#
# From an equality, we can build an equivalence of substitutions:
stmt (SubstBuilderReplacement () ()
(→ (= s t) (↔ (subst s x φ) (subst t x φ))))
stmt (buildSubstReplacement () ((= s t))
(↔ (subst s x φ) (subst t x φ)))
#
# A statement of the form `x = s → (φ ↔ ψ)`

, where `x`

is not free in `ψ`

, can be thought of as an ''implicit substitution'', as it can be used to relate a formula about `x`

to a formula about `s`

. The distinct variable constraint between `x`

and `s`

might be one we can eliminate, but in practice it isn't too difficult to deal with.
stmt (makeSubstExplicit ((s x) (ψ x))
((→ (= x s) (↔ φ ψ)))
(↔ (subst s x φ) ψ))
#
# We can add `subst`

to both sides of an implication or a biconditional.
stmt (SubstAddition () () (→ (∀ x (→ φ ψ)) (→ (subst s x φ) (subst s x ψ))))
stmt (SubstBuilder () () (→ (∀ x (↔ φ ψ)) (↔ (subst s x φ) (subst s x ψ))))
stmt (addSubst () ((→ φ ψ)) (→ (subst s x φ) (subst s x ψ)))
stmt (buildSubst () ((↔ φ ψ)) (↔ (subst s x φ) (subst s x ψ)))
#
# We can move `subst`

across logical connectives,
stmt (SubstNegation () () (↔ (subst s x (¬ φ)) (¬ (subst s x φ))))
stmt (SubstDisjunction () () (↔ (subst s x (∨ φ ψ)) (∨ (subst s x φ) (subst s x ψ))))
stmt (SubstConjunction () () (↔ (subst s x (∧ φ ψ)) (∧ (subst s x φ) (subst s x ψ))))
stmt (SubstImplication () () (↔ (subst s x (→ φ ψ)) (→ (subst s x φ) (subst s x ψ))))
stmt (SubstBiconditional () () (↔ (subst s x (↔ φ ψ)) (↔ (subst s x φ) (subst s x ψ))) )
#
# and quantifiers (to distinct variables).
# Not sure how to make this one work with ghilbert freeness, and we don't seem to be using it.
stmt (SubstThereExists ((s y)) () (↔ (subst s x (∃ y φ)) (∃ y (subst s x φ))))
#
# === Substitution of a variable which does not appear ===
stmt (NullSubstitution ((φ x)) () (↔ (subst s x φ) φ))
#
# === Turning substitution into there-exists ===
# One way to prove a formula of the form `∃ x φ`

is to demonstrate a particular `x`

for which `φ`

holds.
stmt (ThereExistsIntroductionFromObject () () (→ (subst s x φ) (∃ x φ)))
stmt (introduceThereExistsFromObject () ((subst s x φ)) (∃ x φ))
#
# === Specialization ===
# Specialization as conventionally cited contains a substitution, and is often worded something like "if a formula holds for all values of a variable, it also holds when a particular term is properly substituted for that variable" or in symbols `∀ x φ → [ s / x ] φ`

.[http://us.metamath.org/mpeuni/stdpc4.html stdpc4] in metamath's set.mm, accessed June 9, 2010a5sbc in Raph Levien's [http://levien.com/garden/ghnew/peano/ Peano], accessed June 9, 2010Hirst and Hirst, axiom 4 on page 51
stmt (SpecializationToObject () () (→ (∀ x φ) (subst s x φ)))
stmt (specializeToObjectInConsequent () ((→ antecedent (∀ x φ))) (→ antecedent (subst s x φ)))
#
# === Changing the quantified variable ===
# We can transform a quantified formula by substituting each of the occurences of the variable we are quantifying over to another variable, and changing the variable in the quantifier accordingly. Here is a version with implicit substitution,
stmt (ChangeVariableThereExists
((φx y) (φy x) )
((→ (= x y) (↔ φx φy)))
(↔ (∃ x φx) (∃ y φy)))
stmt (ChangeVariableForAll ((φx y) (φy x) )
((→ (= x y) (↔ φx φy)))
(↔ (∀ x φx) (∀ y φy)))
#
# and one with explicit substitution.
stmt (ChangeVariableExplicitThereExists ((φ y) ) ()
(↔ (∃ x φ) (∃ y (subst y x φ))))
stmt (ChangeVariableExplicitForAll ((φ y) ) ()
(↔ (∀ x φ) (∀ y (subst y x φ))))
#
# A similar transformation is possible for substitution.
stmt (ChangeVariableSubstitution
((φx y) (φy x) (s y))
((→ (= x y) (↔ φx φy)))
(↔ (subst s x φx) (subst s y φy)))
#
# === More theorems involving subst ===
stmt (EqualitySubst () () (→ (= x s) (↔ φ (subst s x φ))))
stmt (SubstItself () () (↔ (subst x x φ) φ))
#
# === Some theorems related to substitution ===
# Although the following theorems do not refer to substitution with `subst`

, they do express similar ideas.
stmt (ImplicitForAll ((s x) (ψ x)) ((→ (= x s) (↔ φ ψ)))
(↔ (∀ x (→ (= x s) φ)) ψ))
stmt (ImplicitThereExists ((s x) (ψ x)) ((→ (= x s) (↔ φ ψ)))
(↔ (∃ x (∧ (= x s) φ)) ψ))
#
# == Quantifiability ==
# Although the above results do imply the [[Interface:Axiom of quantifiability|axiom of quantifiability]], at least on occasion it is useful directly.
stmt (Quantifiability ((s x)) () (∃ x (= x s)) )
#
# == References ==
#