Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Nonfreeness
wnnf

Next ⟩ df-bj-nnf

Metamath Proof Explorer

Ascii
Structured

Syntax definition wnnf

Description: Syntax for the nonfreeness quantifier.

		Ref	Expression
	Assertion	wnnf	wff Ⅎ' 𝑥 𝜑