Yes! Existential instantiation looks like exactly what I was asking for. There's another answer which talks about the connection to AC: https://math.stackexch

Yes! Existential instantiation looks like exactly what I was asking for. There's another answer which talks about the connection to AC: https://math.stackexchange.com/a/365282/487512 https://math.stackexchange.com/a/365282/487512 But really, the second answer to the question you posted is the real explanation: https://math.stackexchange.com/a/132910/487512 https://math.stackexchange.com/a/132910/487512 Essentially, we're not actually choosing an element from the set. We're defining a new symbol, and saying that it could represent any element in the set. But you can use that symbol pretty much as if it was one particular, but unknown, element of that set. If I have understood this correctly, then if you "choose" some element a from a set X, and prove some proposition P(a), then you have really proved that for all e in X, P(e).