Description: Axiom of Substitution. One of the 5 equality axioms of predicate calculus. The final consequent A. x ( x = y -> ph ) is a way of expressing " y substituted for x in wff ph " (cf. sb6 ). It is based on Lemma 16 of Tarski p. 70 and Axiom C8 of Monk2 p. 105, from which it can be proved by cases.
The original version of this axiom was ax-c15 and was replaced with this shorter ax-12 in Jan. 2007. The old axiom is proved from this one as Theorem axc15 . Conversely, this axiom is proved from ax-c15 as Theorem ax12 .
Juha Arpiainen proved the metalogical independence of this axiom (in the form of the older axiom ax-c15 ) from the others on 19-Jan-2006. See item 9a at https://us.metamath.org/award2003.html .
See ax12v and ax12v2 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.
This axiom scheme is logically redundant (see ax12w ) but is used as an auxiliary axiom scheme to achieve scheme completeness. (Contributed by NM, 22-Jan-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-12 | ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | 0 | cv | ⊢ 𝑥 |
| 2 | vy | ⊢ 𝑦 | |
| 3 | 2 | cv | ⊢ 𝑦 |
| 4 | 1 3 | wceq | ⊢ 𝑥 = 𝑦 |
| 5 | wph | ⊢ 𝜑 | |
| 6 | 5 2 | wal | ⊢ ∀ 𝑦 𝜑 |
| 7 | 4 5 | wi | ⊢ ( 𝑥 = 𝑦 → 𝜑 ) |
| 8 | 7 0 | wal | ⊢ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) |
| 9 | 6 8 | wi | ⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) |
| 10 | 4 9 | wi | ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |