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	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-5	$$⊢\phi \to \forall y\phi$$
2		ax-12	$$⊢x=y\to \left(\forall y\phi \to \forall x\left(x=y\to \phi \right)\right)$$
3	1 2	syl5	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$