Syntax Definition wc 3

Description: If a and b are terms, a C b is a wff.

Hypotheses

Ref	Expression
wva	term a
wvb	term b

Assertion

Ref	Expression
wc	wff a C b

See definition df-c1 124 for more information.

metamath.org