| 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
https://groups.google.com/g/metamath/c/cteNUppB6A4). |
