Definition df-psub-D6.2 716

Description: Definition of Proper Substitution, '[𝑡 / 𝑥]𝜑'. Read as "The formula resulting from properly substituting '𝑡' for '𝑥' in '𝜑'".

'𝑦' is distinct from all other variables.

Assertion

Ref	Expression
df-psub-D6.2	⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

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

Detailed syntax breakdown of Definition df-psub-D6.2

Step	Hyp	Ref	Expression
1		wff-ph	. . 3 wff 𝜑
2		term-t	. . 3 term 𝑡
3		objvar-x	. . 3 objvar 𝑥
4	1, 2, 3	wff-psub 714	. 2 wff [𝑡 / 𝑥]𝜑
5		objvar-y	. . . . . 6 objvar 𝑦
6	5	term-obj 1	. . . . 5 term 𝑦
7	6, 2	wff-equals 6	. . . 4 wff 𝑦 = 𝑡
8	3	term-obj 1	. . . . . . 7 term 𝑥
9	8, 6	wff-equals 6	. . . . . 6 wff 𝑥 = 𝑦
10	9, 1	wff-imp 10	. . . . 5 wff (𝑥 = 𝑦 → 𝜑)
11	10, 3	wff-forall 8	. . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
12	7, 11	wff-imp 10	. . 3 wff (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
13	12, 5	wff-forall 8	. 2 wff ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
14	4, 13	wff-bi 104	1 wff ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This definition is referenced by:  dfpsubv-P6  717  exipsub-P6  720  specpsub-P6  721  isubtopsub-P6  729  psubtoisub-P6  765  dfpsubalt-P6  774  psubleq-P6  783  psubnfr-P6  784  psubthm-P6  786  psubneg-P6  788  psubim-P6-L1  789