Syntax Definition wfun 5192

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

Hypothesis

Ref	Expression
cA	class 𝐴

Assertion

Ref	Expression
wfun	wff Fun 𝐴

See definition df-fun 5200 for more information.