Theorem solvesub-P6a 704

Description: Solve for Substitution Formula ('𝑥' does not occur in '𝑡').

Requires the existence of '𝜓₁(𝑥₁)' as a replacement for '𝜓(𝑥)'. Also, '𝑥' cannot occur in '𝑡'.

The idea here is that we replace all free occurences of '𝑥' in '𝜑' with '𝑡', first changing any bound variables that conflict with '𝑡' with fresh variables. The result of this process, which is guaranteed to exist, will be called '𝜓'. So long as '𝑥' does not appear in '𝑡', '𝑥' will not occur free in the result, '𝜓'. This fact is needed to prove this statement.

Using the process described above, the existence of a formula, '𝜓', that satisfies the hypotheses of this statement can be proven through induction on formula length. With the assumption that such a formula exists, this statement then "solves" for a direct formula that is gauranteed to be logically equivalent to '𝜓' in every case.

The only limitation of this direct formula is the rule that '𝑥' is not allowed to occur in '𝑡'. An even more general formula where '𝑡' is allowed to contain '𝑥' can be produced by applying this substitution twice, recursively, with an intermediate dummy variable. This is shown in solvedsub-P6a 711.

Hypotheses

Ref	Expression
solvesub-P6a.1	⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))
solvesub-P6a.2	⊢ Ⅎ𝑥𝜓
solvesub-P6a.3	⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
solvesub-P6a	⊢ (𝜓 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Distinct variable groups:   𝜓,𝑥₁   𝜓₁,𝑥   𝑡,𝑥   𝑥,𝑥₁

Proof of Theorem solvesub-P6a

Step	Hyp	Ref	Expression
1		solvesub-P6a.3	. . . . 5 ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))
2		imoverbi-P4.30b 479	. . . . 5 ⊢ ((𝑥 = 𝑡 → (𝜑 ↔ 𝜓)) ↔ ((𝑥 = 𝑡 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜓)))
3	1, 2	bimpf-P4.RC 532	. . . 4 ⊢ ((𝑥 = 𝑡 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜓))
4	3	suballinf-P5 594	. . 3 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜓))
5		solvesub-P6a.2	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	qimeqallb-P6 701	. . 3 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜓) ↔ (∃𝑥 𝑥 = 𝑡 → ∀𝑥𝜓))
7		axL6ex-P5 625	. . . . 5 ⊢ ∃𝑥 𝑥 = 𝑡
8	7	thmeqtrue-P4.21a 442	. . . 4 ⊢ (∃𝑥 𝑥 = 𝑡 ↔ ⊤)
9		solvesub-P6a.1	. . . . 5 ⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))
10	9, 5	qremallw-P6 702	. . . 4 ⊢ (∀𝑥𝜓 ↔ 𝜓)
11	8, 10	subimd-P3.40c.RC 330	. . 3 ⊢ ((∃𝑥 𝑥 = 𝑡 → ∀𝑥𝜓) ↔ (⊤ → 𝜓))
12		trueie-P4.22a 444	. . 3 ⊢ ((⊤ → 𝜓) ↔ 𝜓)
13	4, 6, 11, 12	tbitrns-P4.17.RC 431	. 2 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) ↔ 𝜓)
14	13	bisym-P3.33b.RC 299	1 ⊢ (𝜓 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104  ⊤wff-true 153  ∃wff-exists 595  Ⅎwff-nfree 681

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682

This theorem is referenced by:  solvesub-P6a.VR  705  example-E6.01a  706  solvesub-P6b  707  solvedsub-P6a  711