Am Donnerstag, 26. September 2019 20:17:23 UTC+2 schrieb Mario Carneiro: > > > I believe this is false. While I don't think you can derive false, you can > at least derive that the universe has one element and hence distinctors > don't work: > > ...
> > Mario > You are right, of course. I really thought that evening a definition provides a means of replacing parts literally. I should not post after work, I need to be in a better shape for this. @all Thanks for your answers Wolf -- 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/d5932ca6-cc4e-4e65-82c8-3df3d9f2aa9c%40googlegroups.com.
