Syntax Definition wfn 5118

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 5126 for more information.