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 36121
Description: Equivalent form of the axiom of substitution bj-ax12 36056. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 36085 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 36122. Note that in the LHS, the reverse implication holds by equs4 2410 (or equs4v 1996 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 36056), and the forward implication is sbalex 2228.

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 36114 . . . . 5 (∀𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
21imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
3 19.38 1834 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
42, 3syl 17 . . 3 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
5 hbe1a 2133 . . . . . 6 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
65, 1syl 17 . . . . 5 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
7 bj-exlimg 36022 . . . . 5 ((∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))))
86, 7ax-mp 5 . . . 4 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
9 sp 2169 . . . . 5 (∀𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
109imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
118, 10syl 17 . . 3 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
124, 11impbii 208 . 2 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
13 impexp 450 . . 3 (((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1413albii 1814 . 2 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1512, 14bitri 275 1 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wal 1532  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130  ax-12 2164
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator