Syntax Definition wf 5119

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