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

Theorem ax12v 2033
Description: This is essentially axiom ax-12 2032 weakened by additional restrictions on variables. Besides axc11r 2170, this theorem should be the only one referencing ax-12 2032 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 1826, 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 1826 . 2 (𝜑 → ∀𝑦𝜑)
2 ax-12 2032 . 2 (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
31, 2syl5 33 1 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1826  ax-12 2032
This theorem is referenced by:  ax12v2  2034  19.8a  2037  19.8aOLD  2038  axc15  2287  ax12a2OLD  2327  exsb  2452  mo2v  2461  2eu6  2542  bj-ssbequ1  31636  bj-ssbid1ALT  31640  bj-sb  31667  rexsb  39618
  Copyright terms: Public domain W3C validator