Foundation·F13
Transitivity of identity
Chains of equalities compose.
Built from the universal quantifier, conjunction, and implication.
In words
For any x, y, z, If x equals y and y equals z, then x equals z.
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
An axiom of identity, like reflexivity and symmetry; see the logical framework.
Used by
Propose an edit6 published revisions
- 7/12/2026 · Benjamin· Add explicit quantifier, and, and if/then highlight keys alongside both hypotheses and the conclusion. · Similarity override: In-place edit of the published f-eq3 (transitivity) article: only highlight markup and minor In words phrasing changed. Similarity is against sibling identity axioms f-eq1/f-eq2, which state reflexivity/symmetry, distinct from transitivity.what changed →
- 7/12/2026 · Benjamin· Add word-notation highlight markup linking both hypotheses and the conclusion to the In words reading. · Similarity override: This is an in-place edit of the published f-eq3 (transitivity) 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-eq1/f-eq2 (the other identity axioms), naturally close in shape but stating reflexivity/symmetry, distinct claims from transitivity.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 →