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/g/metamath/c/cteNUppB6A4 ).
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wdfat |