On Thursday, December 24, 2020 at 12:26:53 AM UTC+1 [email protected] wrote:
> Does this affect the statement of any axioms? This may affect the MM -> > MM0 translation, which is assuming that ax-7 is stated with no DV > conditions. > No, the axioms are unchanged. For instance for ax-7, I introduced a weakened form ax7v (it is simply ax-7 with an extra DV condition), which is the only statement referencing ax-7, and I proved back ax-7 from it and earlier axioms (theorem ~ax7). All later theorems should reference ax7 instead of ax-7. I added the usage discouragement tag to the comment of ax-7, indicating to use ax7 instead. Benoît -- 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/7b563357-4fba-4546-94bf-825da2389c6cn%40googlegroups.com.
