Description: This is essentially Axiom ax-12 weakened by additional restrictions on variables. Besides axc11r , this theorem should be the only one referencing ax-12 directly.
Both restrictions on variables have their own value. If for a moment we assume x could be set to y , then, after elimination of the tautology y = y , immediately we have ph -> A. y ph for all ph and y , that is ax-5 , a degenerate result.
The second restriction is not necessary, but a simplification that makes the following interpretation easier to see. Since ph textually at most depends on x , we can look at it at some given 'fixed' y . This theorem now states that the truth value of ph will stay constant, as long as we 'vary x around y ' only such that x = y still holds. Or in other words, equality is the finest grained logical expression. If you cannot differ two sets by = , you won't find a whatever sophisticated expression that does. One might wonder how the described variation of x is possible at all. Note that Metamath is a text processor that easily sees a difference between text chunks { x | -. x = x } and { y | -. y = y } . Our usual interpretation is to abstract from textual variations of the same set, but we are free to interpret Metamath's formalism differently, and in fact let x run through all textual representations of sets.
Had we allowed ph to depend also on y , this idea is both harder to see, and it is less clear that this extra freedom introduces effects not covered by other axioms. (Contributed by Wolf Lammen, 8-Aug-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax12v | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 | ⊢ ( 𝜑 → ∀ 𝑦 𝜑 ) | |
| 2 | ax-12 | ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) | |
| 3 | 1 2 | syl5 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |