Theorem solvesub-P6a.VR 705

Description: Variable Restricted Form of solvesub-P6a 704.

'𝑥' cannot occur in either '𝜓' or '𝑡'.

If we know '𝑥' does not occur in '𝜓' ahead of time, we can remove some of the hypotheses.

Hypothesis

Ref	Expression
solvesub-P6a.VR.1	⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))

Assertion

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

Distinct variable groups:   𝜓,𝑥   𝑡,𝑥

Proof of Theorem solvesub-P6a.VR

Dummy variable 𝑥₁ is distinct from all other variables.

Step	Hyp	Ref	Expression
1		biref-P3.33a 297	. . 3 ⊢ (𝜓 ↔ 𝜓)
2	1	rcp-NDIMP0addall 207	. 2 ⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓))
3		nfrv-P6 686	. 2 ⊢ Ⅎ𝑥𝜓
4		solvesub-P6a.VR.1	. 2 ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))
5	2, 3, 4	solvesub-P6a 704	1 ⊢ (𝜓 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104

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:  dfpsubv-P6  717