On 9/22/24 11:01, 'Meta Kunt' via Metamath wrote:
Is this plan sound? Because I seem to struggle with the existential quantor in fz1iso.
I won't try to reply to everything you were trying to do but if you are having the same struggle I used to have with existential quantifiers you might be looking for https://us.metamath.org/mpeuni/exlimddv.html
Its usage in https://us.metamath.org/mpeuni/xpdom2.html is pretty typical. -- 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/77a901b1-3c62-4b6e-895c-21fcba7dd484%40panix.com.
