wff-nfreet - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > wff-nfreet

Syntax Definition wff-nfreet 1114

Description: Extend WFF definition to include the effective non-freeness in a term predicate 'Ⅎ_t𝑥'.

**Hypotheses**
Ref	Expression
term-t	term 𝑡
objvar-x	objvar 𝑥

**Assertion**
Ref	Expression
wff-nfreet	wff Ⅎ_t𝑥 𝑡

See definition df-nfreet-D8.1 1116 for more information.

Colors of variables: wff objvar term class