Description: Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. It states that equality is a right-Euclidean binary relation (this is similar, but not identical, to being transitive, which is proved as equtr ). This axiom scheme is a sub-scheme of Axiom Scheme B8 of system S2 of Tarski, p. 75, whose general form cannot be represented with our notation. Also appears as Axiom C7 of Monk2 p. 105 and Axiom Scheme C8' in Megill p. 448 (p. 16 of the preprint).
The equality symbol was invented in 1557 by Robert Recorde. He chose a pair of parallel lines of the same length because "noe .2. thynges, can be moare equalle".
We prove in ax7 that this axiom can be recovered from its weakened version ax7v where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 should be ax7v . See the comment of ax7v for more details on these matters. (Contributed by NM, 10-Jan-1993) (Revised by BJ, 7-Dec-2020) Use ax7 instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-7 | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | 0 | cv | ⊢ 𝑥 |
| 2 | vy | ⊢ 𝑦 | |
| 3 | 2 | cv | ⊢ 𝑦 |
| 4 | 1 3 | wceq | ⊢ 𝑥 = 𝑦 |
| 5 | vz | ⊢ 𝑧 | |
| 6 | 5 | cv | ⊢ 𝑧 |
| 7 | 1 6 | wceq | ⊢ 𝑥 = 𝑧 |
| 8 | 3 6 | wceq | ⊢ 𝑦 = 𝑧 |
| 9 | 7 8 | wi | ⊢ ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) |
| 10 | 4 9 | wi | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) ) |