Theorem psubnfr-P6 784

Description: Proper Substitution Applied to ENF Variable.

If '𝑥' is effectively not free in '𝜑', then replacing '𝑥' with some '𝑡' through proper substitution has no effect on '𝜑'.

Hypothesis

Ref	Expression
psubnfr-P6.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
psubnfr-P6	⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)

Proof of Theorem psubnfr-P6

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-psub-D6.2 716	. 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		psubnfr-P6.1	. . . . . 6 ⊢ Ⅎ𝑥𝜑
3	2	qimeqallb-P6 701	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ (∃𝑥 𝑥 = 𝑦 → ∀𝑥𝜑))
4		axL6ex-P5 625	. . . . . . 7 ⊢ ∃𝑥 𝑥 = 𝑦
5	4	thmeqtrue-P4.21a 442	. . . . . 6 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ⊤)
6	2	qremall-P6 722	. . . . . 6 ⊢ (∀𝑥𝜑 ↔ 𝜑)
7	5, 6	subimd-P3.40c.RC 330	. . . . 5 ⊢ ((∃𝑥 𝑥 = 𝑦 → ∀𝑥𝜑) ↔ (⊤ → 𝜑))
8		trueie-P4.22a 444	. . . . 5 ⊢ ((⊤ → 𝜑) ↔ 𝜑)
9	3, 7, 8	dbitrns-P4.16.RC 429	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
10	9	subimr-P3.40b.RC 328	. . 3 ⊢ ((𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ (𝑦 = 𝑡 → 𝜑))
11	10	suballinf-P5 594	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝑡 → 𝜑))
12		qimeqallbv-P5 620	. . 3 ⊢ (∀𝑦(𝑦 = 𝑡 → 𝜑) ↔ (∃𝑦 𝑦 = 𝑡 → ∀𝑦𝜑))
13		axL6ex-P5 625	. . . . 5 ⊢ ∃𝑦 𝑦 = 𝑡
14	13	thmeqtrue-P4.21a 442	. . . 4 ⊢ (∃𝑦 𝑦 = 𝑡 ↔ ⊤)
15		qremallv-P5 656	. . . 4 ⊢ (∀𝑦𝜑 ↔ 𝜑)
16	14, 15	subimd-P3.40c.RC 330	. . 3 ⊢ ((∃𝑦 𝑦 = 𝑡 → ∀𝑦𝜑) ↔ (⊤ → 𝜑))
17	12, 16, 8	dbitrns-P4.16.RC 429	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → 𝜑) ↔ 𝜑)
18	1, 11, 17	dbitrns-P4.16.RC 429	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  [wff-psub 714

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  ax-L12 29

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  df-psub-D6.2 716

This theorem is referenced by:  psubnfr-P6.VR  785  psuball1-P6  793  psubex1-P6  794