Theorem bj-substax12 36687

Description: Equivalent form of the axiom of substitution bj-ax12 36623. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 36651 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 36688. Note that in the LHS, the reverse implication holds by equs4 2424 (or equs4v 1999 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 36623), and the forward implication is sbalex 2243.

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

Step	Hyp	Ref	Expression
1		bj-modal4 36680	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))
2	1	imim2i 16	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))
3		19.38 1837	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
4	2, 3	syl 17	. . 3 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5		hbe1a 2144	. . . . . 6 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	5, 1	syl 17	. . . . 5 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))
7		bj-exlimg 36589	. . . . 5 ⊢ ((∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))))
8	6, 7	ax-mp 5	. . . 4 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))
9		sp 2184	. . . . 5 ⊢ (∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
10	9	imim2i 16	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
11	8, 10	syl 17	. . 3 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
12	4, 11	impbii 209	. 2 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
13		impexp 450	. . 3 ⊢ (((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))
14	13	albii 1817	. 2 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))
15	12, 14	bitri 275	1 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778

This theorem is referenced by: (None)