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 5896), 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 41212, very difficult, 3 apostrophes '''
are used now so that it's
easier to distinguish from df-fv 5896 and df-ima 5127. 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). |
