Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-substax12 Structured version   Visualization version   GIF version

Theorem bj-substax12 36723
Description: Equivalent form of the axiom of substitution bj-ax12 36659. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 36687 on 𝑡, 𝜑) to hold, their equivalence holds without DV conditions. The forward implication is proved in modal (K4) while the reverse implication is proved in modal (T5). The LHS has the advantage of not involving nested quantifiers on the same variable. Its metaweakening is proved from the core axiom schemes in bj-substw 36724. Note that in the LHS, the reverse implication holds by equs4 2420 (or equs4v 1998 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 36659), and the forward implication is sbalex 2241.

The LHS can be read as saying that if there exists a variable equal to a given term witnessing a given formula, then all variables equal to that term also witness that formula. The equivalent form of the LHS using only primitive symbols is (∀𝑥(𝑥 = 𝑡𝜑) ∨ ∀𝑥(𝑥 = 𝑡 → ¬ 𝜑)), which expresses that a given formula is true at all variables equal to a given term, or false at all these variables. An equivalent form of the LHS using only the existential quantifier is ¬ (∃𝑥(𝑥 = 𝑡𝜑) ∧ ∃𝑥(𝑥 = 𝑡 ∧ ¬ 𝜑)), which expresses that there can be no two variables both equal to a given term, one witnessing a formula and the other witnessing its negation. These equivalences do not hold in intuitionistic logic. The LHS should be the preferred form, and has the advantage of having no negation nor nested quantifiers. (Contributed by BJ, 21-May-2024.) (Proof modification is discouraged.)

Assertion
Ref Expression
bj-substax12 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))

Proof of Theorem bj-substax12
StepHypRef Expression
1 bj-modal4 36716 . . . . 5 (∀𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
21imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
3 19.38 1838 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
42, 3syl 17 . . 3 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
5 hbe1a 2143 . . . . . 6 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
65, 1syl 17 . . . . 5 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
7 bj-exlimg 36625 . . . . 5 ((∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))))
86, 7ax-mp 5 . . . 4 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
9 sp 2182 . . . . 5 (∀𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
109imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
118, 10syl 17 . . 3 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
124, 11impbii 209 . 2 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
13 impexp 450 . . 3 (((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1413albii 1818 . 2 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1512, 14bitri 275 1 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1537  wex 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-10 2140  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator