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

Theorem ax12v 2168
Description: This is essentially axiom ax-12 2167 weakened by additional restrictions on variables. Besides axc11r 2379, this theorem should be the only one referencing ax-12 2167 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 1902, 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 1902 . 2 (𝜑 → ∀𝑦𝜑)
2 ax-12 2167 . 2 (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
31, 2syl5 34 1 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1902  ax-12 2167
This theorem is referenced by:  ax12v2  2169  19.8a  2170  sbequ1  2240  axc16g  2252  exsb  2371  axc15  2438  axc15OLD  2439  dfmoeu  2614  2eu6  2740  bj-ax12v  33887  bj-ssbid1ALT  33896  bj-sb  33919  rexsb  43178
  Copyright terms: Public domain W3C validator