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

Theorem bj-subst 34168
 Description: Equivalent form of the axiom of substitution bj-ax12 34103. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 34132 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 34169. Note that in the LHS, the reverse implication holds by equs4 2427 (or equs4v 2006 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 34103). 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-subst ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))

Proof of Theorem bj-subst
StepHypRef Expression
1 bj-modal4 34161 . . . . 5 (∀𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
21imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
3 19.38 1840 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
42, 3syl 17 . . 3 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
5 hbe1a 2145 . . . . . 6 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
65, 1syl 17 . . . . 5 (∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))
7 bj-exlimg 34069 . . . . 5 ((∃𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑))))
86, 7ax-mp 5 . . . 4 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)))
9 sp 2180 . . . . 5 (∀𝑥𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
109imim2i 16 . . . 4 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
118, 10syl 17 . . 3 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) → (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
124, 11impbii 212 . 2 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)))
13 impexp 454 . . 3 (((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1413albii 1821 . 2 (∀𝑥((𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
1512, 14bitri 278 1 ((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator