Metamath Proof Explorer


Theorem ax12v

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 ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 ax-5 ( 𝜑 → ∀ 𝑦 𝜑 )
2 ax-12 ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
3 1 2 syl5 ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )