Maybe I'm missing something but my high level goal is to prove:
|- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c )
using:
|- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )
As pointed by Jim, the easier way to do this is to use ~rspcev and avoid
the explicit substitution. You will need to prove:
|- ( c = 1 -> ( A. x e. RR ( abs ` ( F ` x ) ) <_ c <-> A. x e. RR ( abs
` ( F ` x ) ) <_ 1 ) )
In my case, MMJ2 often automatically fills in ~cbvral, but the right
theorem for that step is ~ralbidv.
--
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/e5d2f406-8edd-75fa-0fd9-9440affad7ab%40gmx.net.
