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