Theorem bj-subst 34434

Description: Equivalent form of the axiom of substitution bj-ax12 34369. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 34398 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 34435. Note that in the LHS, the reverse implication holds by equs4 2428 (or equs4v 2007 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 34369).

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

Step	Hyp	Ref	Expression
1		bj-modal4 34427	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))
2	1	imim2i 16	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))
3		19.38 1841	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
4	2, 3	syl 17	. . 3 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5		hbe1a 2146	. . . . . 6 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	5, 1	syl 17	. . . . 5 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))
7		bj-exlimg 34335	. . . . 5 ⊢ ((∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))))
8	6, 7	ax-mp 5	. . . 4 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))
9		sp 2181	. . . . 5 ⊢ (∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
10	9	imim2i 16	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
11	8, 10	syl 17	. . 3 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
12	4, 11	impbii 212	. 2 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
13		impexp 455	. . 3 ⊢ (((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))
14	13	albii 1822	. 2 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))
15	12, 14	bitri 278	1 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2143  ax-12 2176

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783

This theorem is referenced by: (None)