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 36251
Description: Equivalent form of the axiom of substitution bj-ax12 36186. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 36215 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 36252. Note that in the LHS, the reverse implication holds by equs4 2409 (or equs4v 1995 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 36186), and the forward implication is sbalex 2230.

The LHS can be read as saying that if there exists a setvar equal to a given term witnessing 𝜑, then all setvars equal to that term also witness 𝜑. An equivalent suggestive form for the LHS is ¬ (∃𝑥(𝑥 = 𝑡𝜑) ∧ ∃𝑥(𝑥 = 𝑡 ∧ ¬ 𝜑)), which expresses that there can be no two variables both equal to a given term, one witnessing 𝜑 and the other witnessing ¬ 𝜑. (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 36244 . . . . 5 (∀𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
21imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
3 19.38 1833 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
42, 3syl 17 . . 3 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
5 hbe1a 2132 . . . . . 6 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
65, 1syl 17 . . . . 5 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
7 bj-exlimg 36152 . . . . 5 ((∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))))
86, 7ax-mp 5 . . . 4 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
9 sp 2171 . . . . 5 (∀𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
109imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
118, 10syl 17 . . 3 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
124, 11impbii 208 . 2 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
13 impexp 449 . . 3 (((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1413albii 1813 . 2 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1512, 14bitri 274 1 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1531  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator