wff-nfree - bfol.mm Proof Explorer

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

Syntax Definition wff-nfree 681

Description: Extend WFF definition to include the effective non-freeness predicate 'Ⅎ'.

**Hypotheses**
Ref	Expression
wff-ph	wff 𝜑
objvar-x	objvar 𝑥

**Assertion**
Ref	Expression
wff-nfree	wff Ⅎ𝑥𝜑

See definition df-nfree-D6.1 682 for more information.

Colors of variables: wff objvar term class