Is anyone willing to give me a little help with this error? E-PR-0009 Theorem iocinico.Step 79: Step 79: Label ss2abdv: VerifyProof: DjVars restriction violated! The step lists <ph x> as a DjVars restriction, but the substitutions share variable x.
I'm no sure I understand what a DjVars restriction is or how to fix it. I think it's something to do with having enough distinct variables in an expression, like you can't have S. f(x) dx or something? Any help appreciated, here is the offending line. 78::id |- ( ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) -> x e. ( B [,] B ) ) -> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) -> x e. ( B [,] B ) ) ) 79:78:ss2abdv <http://us.metamath.org/mpegif/ss2abdv.html>|- ( ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) -> x e. ( B [,] B ) ) -> { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) } C_ { x | x e. ( B [,] B ) } ) Here <https://pastebin.com/gPwX3SWf> is the full proof. -- 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/e84d0c8c-4eb2-4c05-99fd-a4af1c0c3072%40googlegroups.com.
