Syntax Definition wfn 4897

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

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵

Assertion

Ref	Expression
wfn	wff 𝐴 Fn 𝐵

See definition df-fn 4905 for more information.