The differnce is that ~eqsb3lem requires x and y to be distinct (because of `$d x y $.`), whereas ~eqsb3 does not have this restriction (x and y may be replaced by the same setvar variable z: `( [ z / z ] z = A <-> z = A )` also holds, see also ~sbid).
On Wednesday, May 3, 2023 at 7:21:57 PM UTC+2 [email protected] wrote: > Looking at them again I guess things are not that simple, because they are > touched by the same person on two consecutive days. > > 在2023年5月3日星期三 UTC+2 00:22:07<David A. Wheeler> 写道： > >> >> >> > On May 2, 2023, at 4:08 PM, Zheng Fan <[email protected]> wrote: >> > >> > Why do we have these two identical lemmas in the database, none of >> which has any discouragement tag? >> >> Probably because no one noticed. >> >> --- 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/8a25bc21-85b4-4c06-867b-92e51dd2744an%40googlegroups.com.
