Bergmann The Logic Book Section 10.1.
There is a rule for adding a Existential Quantifier, Existential Introduction (also commonly known as 'Existential Generalization'). This permits the step illustrated by the following proof fragments.
To understand what this rule permits, it helps to think about it as though you were going backwards from line 6 to line 5. Take the scope of line 6, which is Fx, Fx, and (Fz&Gb) respectively, then substitute a constant for free occurrences of the variable of quantification-- you should be able to get line 5, and indeed you can.
The Rule of Existential Introduction ∃I
If a derivation contains a line of the form
n. <formula>[<constant>/<variable>] <any justification>
then a line of the form
(∃<variable>)<formula> 'n ∃I'
may be added to the derivation.
Notice that, in a sense, you are generalizing on occurrences of the constant in the first formula. Now, you do not have to generalize on all of them; you can generalize on 0, 1, or many, depending on what is there and what you want to do.
Exercise to accompany Predicate Tutorial 10
Exercise 1 (of 1)
Derive the following