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 ". In a previous version, the symbol " ' " was used. However, since the similarity with the symbol ` `` used for the current definition of a function's value (see df-fv ), which, by the way, was intended to visualize that in many cases `` and " ' " are exchangeable, makes reading the theorems, especially those which use both definitions as dfafv2 , very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv and df-ima . And not three backticks ( three times `` ` ) since that would be annoying to escape in a comment. (See remark of Norman Megill and Gerard Lang at https://groups.google.com/g/metamath/c/cteNUppB6A4 ).
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cafv | class ( F ''' A ) |