Theorem solvedsub-P6a 711

Description: Solve for Double Substitution Formula ('𝑥' may occur in '𝑡').

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

The idea is the same as in solvesub-P6a 704, but we perform two substitutions in sequence. We first replace all free occurences of '𝑥' in '𝜑' with a fresh variable '𝑦' to get '𝜓'. We then replace all free occurences of '𝑦' in '𝜓' with '𝑡' (remembering to change any conflicting bound variables) in order to obtain '𝜒'.

The double substitution above is needed to allow '𝑥' to occur in the term '𝑡'. Again, it can be proved inductively that the formulas '𝜓' and '𝜒', obtained by the double substitution described above, satisfy the hypotheses of this statement. We can then "solve" for an equivalent direct formula.

Hypotheses

Ref	Expression
solvedsub-P6a.1	⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))
solvedsub-P6a.2	⊢ Ⅎ𝑥𝜓
solvedsub-P6a.3	⊢ (𝑦 = 𝑦₁ → (𝜒 ↔ 𝜒₁))
solvedsub-P6a.4	⊢ Ⅎ𝑦𝜒
solvedsub-P6a.5	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
solvedsub-P6a.6	⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
solvedsub-P6a	⊢ (𝜒 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

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

Proof of Theorem solvedsub-P6a

Step	Hyp	Ref	Expression
1		solvedsub-P6a.3	. . 3 ⊢ (𝑦 = 𝑦₁ → (𝜒 ↔ 𝜒₁))
2		solvedsub-P6a.4	. . 3 ⊢ Ⅎ𝑦𝜒
3		solvedsub-P6a.6	. . 3 ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))
4	1, 2, 3	solvesub-P6a 704	. 2 ⊢ (𝜒 ↔ ∀𝑦(𝑦 = 𝑡 → 𝜓))
5		solvedsub-P6a.1	. . . . 5 ⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))
6		solvedsub-P6a.2	. . . . 5 ⊢ Ⅎ𝑥𝜓
7		solvedsub-P6a.5	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
8	5, 6, 7	solvesub-P6a 704	. . . 4 ⊢ (𝜓 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
9	8	subimr-P3.40b.RC 328	. . 3 ⊢ ((𝑦 = 𝑡 → 𝜓) ↔ (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
10	9	suballinf-P5 594	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → 𝜓) ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
11	4, 10	bitrns-P3.33c.RC 303	1 ⊢ (𝜒 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104  Ⅎ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:  example-E6.02a  712  solvedsub-P6b  713