Syntax Definition wn 4

Description: If a is a term, a_|_ is a wff.

Hypothesis

Ref	Expression
wva	term a

Assertion

Ref	Expression
wn	term a_|_

This syntax is primitive. The first axiom using it is ax-a1 29.

metamath.org