The goal of rspc.2 is to state that `ps` is the same as `ph`, with all instances of `x` replaced by `A.
So logically there should not be any instance of `x` remaining in `ps`. There are two ways to state this constraint: * the first way is using the "distinct variable conditions", which is used in `~ rspcv` <https://us.metamath.org/mpeuni/rspcv.html> * the second way is using a "not free" hypothesis, which is indeed what `rspc.1` is for. On the website page, the "allowed substitution hint" lists all substitutions which are not forbidden in the first way, by a "distinct variable conditions". It is a facility which is built automatically, but does not take the "not free hypotheses" into account, therefore the name "/hint/". So you're right to point out that that in this case, while it's not disallowed by distinct variable conditions, it's actually disallowed by the not free hypothesis `rspc.1` BR, _ Thierry On 01/03/2025 17:11, bil...@gmail.com wrote:
Theorem rspc has the allowed substitution hint ps(x). Is this correct? Doesn't the hypothesis rspc.1 say that x does not depend on x? -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/metamath/c8a236ac-28c6-4d04-a221-f2a556ee8819n%40googlegroups.com <https://groups.google.com/d/msgid/metamath/c8a236ac-28c6-4d04-a221-f2a556ee8819n%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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 metamath+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/metamath/ad0d659c-2da9-48b8-8ecc-b2a1796acd2c%40gmx.net.
