Syntax Definition wf 5254

Description: Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps 𝐴 into 𝐵.)

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵
cF	class 𝐹

Assertion

Ref	Expression
wf	wff 𝐹:𝐴⟶𝐵

See definition df-f 5262 for more information.