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

Syntax Definition wdfat 43625
Description: Extend the definition of a wff to include the "defined at" predicate. Read: "(the function) 𝐹 is defined at (the argument) 𝐴". In a previous version, the token "def@" was used. However, since the @ is used (informally) as a replacement for $ in commented out sections that may be deleted some day. While there is no violation of any standard to use the @ in a token, it could make the search for such commented-out sections slightly more difficult. (See remark of Norman Megill at
Ref Expression
cA class 𝐴
cF class 𝐹
Ref Expression
wdfat wff 𝐹 defAt 𝐴

See definition df-dfat 43628 for more information.

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