St Anselm's ontological argument

In Appendix 4 of Meaning and Argument (Blackwell, 2003), Ernest Lepore sets the task of symbolizing in FOL the following argument:

The perfect being has all positive perfections. Existence is a perfection. So, the perfect being has existence.

This is of course Anselm of Canterbury's ontological argument for the existence of God. The argument has received so much attention and criticism since it was first formulated in the 11th century that no purpose would be served to rehearse any of that here. However, I have only ever seen it proved within the scope of modal logic, so here is my symbolization in first order logic and the subsequent proof. The proof is quite straightforward.

Key:

Px - x is fully perfect ('has all positive perfections')

g - the perfect being

1. (x)(Px ⊃x = g)
2. (∃x)Px
3. ∴(∃x) x = g
4. Pa / 2EI
5. Pa ⊃a = g / 1UI
6. a = g / 4,5MP
7. (∃x) x = g / 6EG