G {\displaystyle G} is a setw and ⋅ {\displaystyle \cdot } a binary operationw, a b := a ⋅ b {\displaystyle ab:=a\cdot b} , then
( G , ⋅ ) i s a g r o u p :⇔ ∀ x ∈ G , y ∈ G x y ∈ G ∧ ∀ x ∈ G , y ∈ G , z ∈ G ( x y ) z = x ( y z ) ∧ ∃ e ∈ G ∀ x ∈ G ( x e = x = e x ∧ ∃ y ∈ G y x = e = x y ) {\displaystyle (G,\cdot )\ is\ a\ group:\Leftrightarrow {\underset {x\in G,\,y\in G}{\forall }}xy\in G\land {\underset {x\in G,\,y\in G,\,z\in G}{\forall }}(xy)z=x(yz)\land {\underset {e\in G}{\exists }}\ {\underset {x\in G}{\forall }}\left(xe=x=ex\land {\underset {y\in G}{\exists }}yx=e=xy\right)}
∀ e ∈ G , e ′ ∈ G ( ∀ x ∈ G x e = x = e x ∧ ∀ x ∈ G x e ′ = x = e ′ x ⇒ e = e e ′ = e ′ ) {\displaystyle {\underset {e\in G,\,e'\in G}{\forall }}\left({\underset {x\in G}{\forall }}xe=x=ex\land {\underset {x\in G}{\forall }}xe'=x=e'x\Rightarrow e=ee'=e'\right)}
∀ x ∈ G ∀ y ∈ G , z ∈ G ( y x = e = x y ∧ z x = e = x z ⇒ y = e y = ( z x ) y = z ( x y ) = z e = z ) {\displaystyle {\underset {x\in G}{\forall }}\ {\underset {y\in G,\,z\in G}{\forall }}(yx=e=xy\land zx=e=xz\Rightarrow y=ey=(zx)y=z(xy)=ze=z)}
Hence ( G , ⋅ ) i s a g r o u p ⇔ {\displaystyle (G,\cdot )\ is\ a\ group\Leftrightarrow }
∀ x ∈ G , y ∈ G x y ∈ G ∧ ∀ x ∈ G , y ∈ G , z ∈ G ( x y ) z = x ( y z ) ∧ ∃ ! e ∈ G ∀ x ∈ G ( x e = x = e x ∧ ∃ ! y ∈ G ( y x = e = x y , y =: x − 1 ) ) {\displaystyle {\underset {x\in G,\,y\in G}{\forall }}xy\in G\land {\underset {x\in G,\,y\in G,\,z\in G}{\forall }}(xy)z=x(yz)\land {\underset {e\in G}{\exists !}}\ {\underset {x\in G}{\forall }}\left(xe=x=ex\land {\underset {y\in G}{\exists !}}\left(yx=e=xy,\,y=:x^{-1}\right)\right)}