Definition df-nfreet-D8.1 1116

Description: Definition of Effictive Non-Freeness in a Term, 'Ⅎ_t𝑥 𝑡'.

'𝑦' is distinct from all other variables.

Assertion

Ref	Expression
df-nfreet-D8.1	⊢ (Ⅎt𝑥 𝑡 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝑡)

Distinct variable groups:   𝑡,𝑦   𝑥,𝑦

Detailed syntax breakdown of Definition df-nfreet-D8.1

Step	Hyp	Ref	Expression
1		term-t	. . 3 term 𝑡
2		objvar-x	. . 3 objvar 𝑥
3	1, 2	wff-nfreet 1114	. 2 wff Ⅎt𝑥 𝑡
4		objvar-y	. . . . . 6 objvar 𝑦
5	4	term-obj 1	. . . . 5 term 𝑦
6	5, 1	wff-equals 6	. . . 4 wff 𝑦 = 𝑡
7	6, 2	wff-nfree 681	. . 3 wff Ⅎ𝑥 𝑦 = 𝑡
8	7, 4	wff-forall 8	. 2 wff ∀𝑦Ⅎ𝑥 𝑦 = 𝑡
9	3, 8	wff-bi 104	1 wff (Ⅎt𝑥 𝑡 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝑡)

This definition is referenced by:  nfrzero-P8  1117  nfrvar-P8  1118  nfrsucc-P8  1119  nfradd-P8  1120  nfrmult-P8  1121