Theorem bj-substax12 34903

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

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

Step	Hyp	Ref	Expression
1		bj-modal4 34896	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))
2	1	imim2i 16	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))
3		19.38 1841	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
4	2, 3	syl 17	. . 3 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5		hbe1a 2140	. . . . . 6 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	5, 1	syl 17	. . . . 5 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))
7		bj-exlimg 34804	. . . . 5 ⊢ ((∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))))
8	6, 7	ax-mp 5	. . . 4 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))
9		sp 2176	. . . . 5 ⊢ (∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
10	9	imim2i 16	. . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
11	8, 10	syl 17	. . 3 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
12	4, 11	impbii 208	. 2 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
13		impexp 451	. . 3 ⊢ (((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))
14	13	albii 1822	. 2 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))
15	12, 14	bitri 274	1 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀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 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by: (None)