Foundation·F12
Symmetry of identity
Equality can be read in either direction.
Built from the universal quantifier and implication.
In words
For any x, y, If x equals y then y equals x.
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; see the logical framework.
Used by
Propose an edit5 published revisions
- 7/12/2026 · Benjamin· Add explicit quantifier and if/then highlight keys alongside the hypothesis and conclusion. · Similarity override: In-place edit of the published f-eq2 (symmetry) article: only highlight markup and minor In words phrasing changed. Similarity is against sibling identity axioms f-eq1/f-eq3, which state reflexivity/transitivity, distinct from symmetry.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 →