Theorem trnsvsubw-P6 710

Description: Transitive Dummy Variable Substitution (weakened form).

Requires the existence of '𝜒₁(𝑦₁)' as a replacement for '𝜒(𝑦)'. Also, neither '𝑦' nor '𝑦₁' can occur in '𝜑' and '𝑦' cannot occur in '𝑡'.

Hypotheses

Ref	Expression
trnsvsubw-P6.1	⊢ Ⅎ𝑦𝜒
trnsvsubw-P6.2	⊢ (𝑦 = 𝑦₁ → (𝜒 ↔ 𝜒₁))
trnsvsubw-P6.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
trnsvsubw-P6.4	⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
trnsvsubw-P6	⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜒))

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

Proof of Theorem trnsvsubw-P6

Step	Hyp	Ref	Expression
1		eqmiddle-P6.CL 709	. 2 ⊢ (𝑥 = 𝑡 → ∃𝑦(𝑥 = 𝑦 ∧ 𝑦 = 𝑡))
2		trnsvsubw-P6.3	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		trnsvsubw-P6.4	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))
4	2, 3	joinimandres2-P4.RC 581	. . . 4 ⊢ ((𝑥 = 𝑦 ∧ 𝑦 = 𝑡) → ((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)))
5		bitrns-P3.33c.CL 304	. . . 4 ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)) → (𝜑 ↔ 𝜒))
6	4, 5	syl-P3.24.RC 260	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝑦 = 𝑡) → (𝜑 ↔ 𝜒))
7	6	alloverimex-P5.RC.GEN 603	. 2 ⊢ (∃𝑦(𝑥 = 𝑦 ∧ 𝑦 = 𝑡) → ∃𝑦(𝜑 ↔ 𝜒))
8		trnsvsubw-P6.2	. . . 4 ⊢ (𝑦 = 𝑦₁ → (𝜒 ↔ 𝜒₁))
9	8	subbir-P3.41b 334	. . 3 ⊢ (𝑦 = 𝑦₁ → ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜒₁)))
10		nfrv-P6 686	. . . 4 ⊢ Ⅎ𝑦𝜑
11		trnsvsubw-P6.1	. . . 4 ⊢ Ⅎ𝑦𝜒
12	10, 11	nfrbi-P6 691	. . 3 ⊢ Ⅎ𝑦(𝜑 ↔ 𝜒)
13	9, 12	nfrexgenw-P6 696	. 2 ⊢ (∃𝑦(𝜑 ↔ 𝜒) → (𝜑 ↔ 𝜒))
14	1, 7, 13	dsyl-P3.25.RC 262	1 ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜒))

Syntax hints:  term-obj 1   = wff-equals 6   → wff-imp 10   ↔ wff-bi 104   ∧ wff-and 132  ∃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:  solvedsub-P6b  713