MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax12v Structured version   Visualization version   GIF version

Theorem ax12v 2045
Description: This is essentially axiom ax-12 2044 weakened by additional restrictions on variables. Besides axc11r 2186, this theorem should be the only one referencing ax-12 2044 directly.

Both restrictions on variables have their own value. If for a moment we assume 𝑦 could be set to 𝑥, then, after elimination of the tautology 𝑥 = 𝑥, immediately we have 𝜑 → ∀𝑥𝜑 for all 𝜑 and 𝑥, that is ax-5 1836, a degenerate result.

The second restriction is not necessary, but a simplification that makes the following interpretation easier to see. Since 𝜑 textually at most depends on 𝑥, we can look at it at some given 'fixed' 𝑦. This theorem now states that the truth value of 𝜑 will stay constant, as long as we 'vary 𝑥 around 𝑦' only such that 𝑥 = 𝑦 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 𝑥 is possible at all. Note that Metamath is a text processor that easily sees a difference between text chunks {𝑥 ∣ ¬ 𝑥 = 𝑥} and {𝑦 ∣ ¬ 𝑦 = 𝑦}. 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 𝑥 run through all textual representations of sets.

Had we allowed 𝜑 to depend also on 𝑦, 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.)

Assertion
Ref Expression
ax12v (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ax12v
StepHypRef Expression
1 ax-5 1836 . 2 (𝜑 → ∀𝑦𝜑)
2 ax-12 2044 . 2 (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
31, 2syl5 34 1 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1836  ax-12 2044
This theorem is referenced by:  ax12v2  2046  19.8a  2049  19.8aOLD  2050  axc15  2302  ax12a2OLD  2342  exsb  2467  mo2v  2476  2eu6  2557  bj-ssbequ1  32339  bj-ssbid1ALT  32343  bj-sb  32372  rexsb  40502
  Copyright terms: Public domain W3C validator