**Description: **Extend the definition of
a class to include the value of a function.
(Read: The value of 𝐹 at 𝐴, or "𝐹 of
𝐴."). 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 5855), which, by the way, was intended to
visualize that in many cases ‘ and " '
" are exchangeable, makes
reading the theorems, especially those which uses both definitions as
dfafv2 40516, very difficult, 3 apostrophes ''' are used now so that it's
easier to distinguish from df-fv 5855 and df-ima 5087. 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/forum/#!topic/metamath/cteNUppB6A4). |