cfv - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition cfv 3182

Description: Extend the definition of a class to include the value of a function. (Read: The value of F at A, or "F of A".)

**Hypotheses**
Ref	Expression
cA	class A
cF	class F

**Assertion**
Ref	Expression
cfv	class (F ‘A)

See definition df-fv 3198 for more information.

Colors of variables: wff set class