How to write an implication whose antecedent quantifies a variable in its consequent? I want to write the statement
$$\text{If } A^{-1} \text{ exists then } A^{-1} = \frac{\alpha-a}{\alpha^2-a^2}$$
using quantifiers. Note that $A$ and its inverse, if it exists, are taken from the set $\mathscr{G}$. My first thought is
$$ \exists B \in \mathscr{G}, BA = 1 \to B = \frac{\alpha - a}{\alpha^2 - a^2}$$
but this is incorrect because the antecedent needs to include the quantifier while here the grouping works out like so:
$$ \exists B \in \mathscr{G} \left( BA = 1 \to B = \frac{\alpha - a}{\alpha^2 - a^2} \right).$$
This is still true if $A^{-1}$ does not exist; in this case, there is simply no $B$ that satisfies the antecedent. But this is not the statement I'm looking for, because I need the quantifier in the antecedent. But the difficulty is that with the quantifier in the antecedent, there's no way to "instantiate" $B$ in the consequent:
$$ \left( \exists B \in \mathscr{G} , BA = 1 \right) \to \left( \underbrace{B}_\text{Not the same $B$.} = \frac{\alpha - a}{\alpha^2 - a^2} \right). $$
I believe that in first order logic you can say, "if there exists some $x$ satisfying these properties, then let this variable here be that $x$." How do I write that in this context?
 A: Your statement is what is called a 'donkey-sentence', named after the rather violent example of:
'If a farmer owns a donkey, he will beat it'
Note how if you are asked to symbolize this one, you are likely to go through the same thought process you went through:
The first thought is that it is a conditional:
$\exists x \ \exists y (F(x) \land D(y) \land O(x,y)) \to B(x,y)$
But this doesn't work, since you have free variables in the consequent.
OK, but if you then pull the scope of the existential over the consequent, you get:
$\exists x \ \exists y ((F(x) \land D(y) \land O(x,y)) \to B(x,y))$
which doesn't work either, since this statement can be made trivially true by picking anything for $x$ that is not a farmer and/or anything for $y$ that is not a donkey, and hence the statement ends up saying little of interest at all.
The correct answer, of course, is to use a universal:
$\forall x \ \forall y ((F(x) \land D(y) \land O(x,y)) \to B(x,y))$
because the 'a' in 'a farmer' and 'a donkey' is really used as 'any'.
Similarly, the correct symbolization of our statement should be:
$$ \forall B \in \mathscr{G} \left( BA = 1 \to B = \frac{\alpha - a}{\alpha^2 - a^2} \right).$$
Now, you may still be wondering why you have a feeling that there should be an existential here.
Well, consider the following modified donkey-sentence:
'If a farmer owns a donkey, then we have a problem'
Now this sentence can be symbolized as:
$\exists x \ \exists y (F(x) \land D(y) \land O(x,y)) \to P$
Moreover, this turns out to be equivalent to:
$\forall x \ \forall y ((F(x) \land D(y) \land O(x,y)) \to P)$
So yes, there is a close connection between the use of the existential and the universal when conditionals are involved.
A: $$\forall A,B \in S ( (AB=I)\implies  B=\dots )$$
Or you can write: for all $A $ in the set (( there is B in the set AB=I) therefore  ($B=\dots$))
A: You can actually just write $$A^{-1} = B \implies B = \frac{\alpha - a}{\alpha^2 - a^2}$$
since the equivalence will only be provable if $A^{-1}$ is defined.
