Understanding Symbolic Logic, Virginia Klenk, 5th edition, Pearson Prentice Hall, 2008, Unit 20, Ex. 2(a), p.381

Construct a proof for the following argument:

1. (x){{Fx • (∃y)[Fy • ¬ (x = y)]} ⊃(Axb ∨Abx)}
2. Fa • Fb
3. Ga • ¬ Gb
4. ∴ Aab ∨Aba
5. ¬ (a = b) ......... 3 Id
6. Fb ......... 2 Simp.
7. Fb • ¬ (a = b) ......... 6,5 Conj.
8. (∃y)[Fy • ¬ (a = y)] ......... 7 EG
9. {Fa • (∃y)[Fy • ¬ (a = y)]} ⊃(Aab ∨Aba) ......... 1 UI x/a
10. Fa ......... 2 Simp.
11. Fa • (∃y)[Fy • ¬ (a = y)] ......... 10,8 Conj.
12. Aab ∨Aba ......... 11,9 MP