For a given type X, rigorously show that idX = (idX)^-1

Question

For a given type X, rigorously show that idX = (idX)^-1

I have done the following so far:

(x,y) ∈ idX

<=> identity relation

x=y ^ x ∈ X

.

.

.

.

y=x ^ y ∈ X

<=> identity relation

(y,x) ∈ idX

<=> relational inverse 

(x,y) ∈ (idX)^-1

Basically I don't know how to connect the two together. Thanks in advance

Answer 1

From $x=y\land x\in X$, we obtain $x=y$ and $x\in X$. Using the equality $x=y$, we can substitute $x$ with $y$ in $x\in X$ and thus obtain $y\in X$. As equality is symmetric, $x=y$ implies $y=x$. So we have $y=x$ and $y\in X$, hence also $y=x\land y\in X$.