Syntax Definition wrel 2415

Description: Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
wrel	wff Rel A

See definition df-rel 2425 for more information.

metamath.org