# The converse of the axiom of extensionality

I read that the converse of

$\forall a \forall b (\forall c (c \in a \leftrightarrow c \in b) \rightarrow a = b)$

follows from the substitution property of equality.

Therefore I did the following, but I am quite sure this is not right. I would greatly appreciate if someone could point me to how to apply the substitution property.

What I tried to do was:

$\phi = \forall c (c \in a \leftrightarrow c \in a)$

Now substituting some occurances of unbound $a$ with unbound $b$:

$\phi' = \forall c (c \in a \leftrightarrow c \in b)$

Using the substitution property:

$\forall a \forall b (a = b \rightarrow (\phi \rightarrow \phi') )$

$\forall a \forall b (a = b \rightarrow (\forall c (c \in a \leftrightarrow c \in a) \rightarrow \forall c (c \in a \leftrightarrow c \in b)) )$

$\forall a \forall b (a = b \rightarrow (\forall c \top \rightarrow \forall c (c \in a \leftrightarrow c \in b)) )$

$\forall a \forall b (a = b \rightarrow (\top \rightarrow \forall c (c \in a \leftrightarrow c \in b)) )$

$\forall a \forall b (a = b \rightarrow \forall c (c \in a \leftrightarrow c \in b))$

This is the expected converse. But does the procedure make any sense?