Hi Jon, Yes this is a distinct variable restriction: x is not allowed to occur in the “ph” of ss2abdv, i.e. in your > ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) > -> x e. ( B [,] B ) ) The solution is maybe to replace x by another set variable. _ Thierry
> Le 10 juin 2019 à 17:46, Jon P <[email protected]> a écrit : > > 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 |- ( ( ( 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 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. -- 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/21B9115B-C54C-492C-B1C7-8543FFED7FC6%40gmx.net.
