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

Syntax Definition wdfat 28073
Description: Extend the definition of a wff to include the "defined at" predicate. (Read: (The Function)  F is defined at (the argument)  A). 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 https://groups.google.com/forum/#!topic/metamath/cteNUppB6A4).
Hypotheses
Ref Expression
cA  class  A
cF  class  F
Assertion
Ref Expression
wdfat  wff  F defAt  A

See definition df-dfat 28076 for more information.

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