Oh cool. I was aware that equals and subset and df-br don't take parentheses but I hadn't quite thought of them as all examples of a "class thing class" (and produce a formula) pattern. I see we have this nicely documented in the "Infix and parentheses" section of conventions.html
On June 5, 2023 8:05:19 AM PDT, "David A. Wheeler" <[email protected]> wrote: >> On Monday, June 5, 2023 at 9:18:51 AM UTC+8 [email protected] wrote: >> '=' stands for class equality: https://us.metamath.org/mpeuni/wceq.html >> (e.g. equality of numbers) >> '↔' stands for the logical biconditional: >> https://us.metamath.org/mpeuni/wb.html (i.e. equality of truth values) > >> On Jun 5, 2023, at 1:26 AM, Humanities Clinic <[email protected]> >> wrote: >> >> Erm yes I know that.. But it's a little confusing when one sign should/can >> be used instead of the other.. Can someone clarify? > >Sure! If the left & right sides are classes (including sets), use "=". >If the left & right sides are wffs (that is, values that are true or false), >use "<->". > >So you'd say A = B and ( ph <-> ps ), not the other way around. >The constant true is represented as "T." and the constant false is "F.", >so you'd compare to them using "<->". Here's a true statement: >( T. <-> A. x x = x ) > >While we're mentioning it, set.mm is picky about parentheses. Here are the >conventions: > >* When a function that takes two classes and produces a class is applied > as part of an infix expression, the expression is always surrounded by > parentheses. For example, the use of "+" in <tt>( 2 + 2 )</tt>. >* Predicate expressions in infix form that take two or three wffs > (a true or false value) and produce a wff are also always > surrounded by parentheses, such as <tt>( ph -> ps )</tt>. >* In contrast, a binary relation > (which compares two classes and produces a wff) > applied in an infix expression is *not* surrounded by parentheses. This > includes set membership, for example, "1 e. RR" (1 is a member > of the set of real numbers) has no parentheses. This also includes "=". > >You can find other set.mm conventions in: >* set.mm general conventions - https://us.metamath.org/mpeuni/conventions.html >* set.mm label naming conventions - >https://us.metamath.org/mpeuni/conventions-labels.html > >--- David A. Wheeler > >-- >You received this message because you are subscribed to the Google Groups >"Metamath" group. >To unsubscribe from this group and stop receiving emails from it, send an >email to [email protected]. >To view this discussion on the web visit >https://groups.google.com/d/msgid/metamath/F49861B9-4EFE-47B5-9DFB-89F4D2D26A48%40dwheeler.com. > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4F18F28D-DE47-4648-986E-2214AC09043B%40panix.com.
