Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cafv Structured version   Visualization version   GIF version

Syntax Definition cafv 43193
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 6356), 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 43208, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6356 and df-ima 5561. 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 5561).
Hypotheses
Ref Expression
cA class 𝐴
cF class 𝐹
Assertion
Ref Expression
cafv class (𝐹'''𝐴)

See definition df-afv 43196 for more information.

Colors of variables: wff setvar class
  Copyright terms: Public domain W3C validator