Deduction, Daniel Bonevac, Blackwell Publishing, 2nd edition, 2003, Ex. 8.3, problem 12

Show that the given statement is a consequence of a formula. To show that it is so, we construct an argument with the first statement as a premise and the second as a conclusion. Two things worth noting about this proof. One: 'y' from line 4 is instantiated to 'a' on line 5 by universal instantiation even though, or perhaps because, we have already instantiated into 'a' by existential instantiation on line 4. Two: this allows us to set up a biconditional which can be easily simplified and the remainder dispatched by Modus Ponens after having first introduced the identity a = a.

1. (∃x)(y)(y = x ≡ Gy)
2. ∴(x)Fx ⊃(∃x)(Gx • Fx)
3. * (x)Fx / ACP
4. * (y)(y = a ≡ Gy) / 1EI x/a
5. * a = a ≡ Ga / 4UI y/a
6. * (a = a ⊃Ga) • (Ga ⊃a = a) / 5BE
7. * a = a ⊃Ga / 6Simp.
8. * a = a / Id
9. * Ga / 8,7MP
10. * Fa / 3UI x/a
11. * Ga • Fa / 9,10Conj.
12. * (∃x)(Gx • Fx) / 11EG
13. (x)Fx ⊃(∃x)(Gx • Fx) / 3-12CP