@Huxley,
E!x, iff, x exists .
E!x =df (some F)(Fx).
E!x <-> (some F)(Fx).
x exists, means, there is some property that x has.
If we can assert that x has a property then we can assert that x exists.
|-. Gx -> E!x.
If x has the property G then x exists.
|-. x=x -> E!x).
If x is self identical then x exists.
|-. E!x <-> Ey(x=y).
x exists, iff, there is some y such that x is equal to it.
|-. H(the x:Gx) -> (the x:Gx) exists.
If (the x such that Gx) has the property H, then, (the x such that Gx) exists.
|-. (the x:Gx)=(the x:Gx) -> E!(the x:Gx).
If, the x such that Gx is self identical then, (the x such that Gx) exists.
|-. E!(the x: Gx) <-> Ey((the x: Gx)=y).
The x such that Gx exists, iff, there is some y such that (the x:Gx) is equal to it.
|-. G(the x:Gx & Hx) -> E!(the x:Gx).
|-. E!(the x:Gx) <-> EyAx(x=y <-> Gx).
E!(the x: x=z) <-> E!z.