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

Theorem ax12v 2170
Description: This is essentially axiom ax-12 2169 weakened by additional restrictions on variables. Besides axc11r 2381, this theorem should be the only one referencing ax-12 2169 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 1904, 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 1904 . 2 (𝜑 → ∀𝑦𝜑)
2 ax-12 2169 . 2 (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
31, 2syl5 34 1 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1904  ax-12 2169
This theorem is referenced by:  ax12v2  2171  19.8a  2172  sbequ1  2242  axc16g  2254  exsb  2373  axc15  2440  axc15OLD  2441  dfmoeu  2616  2eu6  2743  bj-ax12v  33876  bj-ssbid1ALT  33885  bj-sb  33908  rexsb  43166
  Copyright terms: Public domain W3C validator