Syntax Definition wfun 2416

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

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
wfun	wff Fun A

See definition df-fun 2432 for more information.

metamath.org