Syntax Definition wle 2

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

Hypotheses

Ref	Expression
wva	term  a
wvb	term  b

Assertion

Ref	Expression
wle	wff  a ≤ b

See definition df-le1 122 for more information.

metamath.org