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