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?
Thank you in advance.
This seems perfectly reasonable. Whether it's a correct derivation in your particular context will depend on the specific rules your system uses (there are many different proof systems), so you will need to check that, but it seems reasonable.