Foundation·F14
Substitutivity of identity
Equal objects are interchangeable in any property (Leibniz).
Built from the universal quantifier and implication. Formally a schema: one instance for every formula
.
In words
For any property P, x, y, If x equals y then whatever P holds of x also holds of y.
Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.
Remarks
The fourth axiom of identity. Reflexivity (F11), symmetry (F12), and transitivity (F13) make equality an equivalence relation; substitutivity is what makes it genuine identity, the indiscernibility of identicals. The schema states only one direction of substitution; the converse, that a property of
transfers back to
, follows by first flipping the equation with symmetry. Its set-theoretic echo is Extensionality: equal sets have the same members (read substitutivity on the predicate
).
Used by
Propose an edit6 published revisions
- 7/12/2026 · Benjamin· Add explicit quantifier and if/then highlight keys alongside the equality hypothesis and the transferred property. · Similarity override: In-place edit of the published f-eq4 (substitutivity) article: only highlight markup and minor In words phrasing changed. Similarity is against sibling identity axioms f-eq2/f-eq3, which state symmetry/transitivity, distinct from substitutivity.what changed →
- 7/12/2026 · Benjamin· Add word-notation highlight markup linking the equality hypothesis and the transferred property to the In words reading. · Similarity override: This is an in-place edit of the published f-eq4 (substitutivity) article itself, not a new article: only hl()/@key highlight markup is added, the mathematical content is unchanged. The similarity hits are its siblings f-eq2/f-eq3 (the other identity axioms), naturally close in shape but stating symmetry/transitivity, distinct claims from substitutivity.what changed →
- 7/11/2026 · Benjamin· Fix Mathlib link: add the #doc fragment doc-gen4's find endpoint requires (old link 404'd). Content unchanged.what changed →
- 7/11/2026 · Benjamin· Cite the logic layer beneath the identity axiomswhat changed →
- 7/11/2026 · Benjamin· Backfill: add plain-English prose and Mathlib docs linkwhat changed →
- 7/11/2026 · Benjamin· Initial foundations seedwhat changed →