Hi, I have a question related to the axiom of extensionality, why is it expressed with a simple conditional, and not using a biconditional, if I have two equal sets, I cannot imply that they have the same objects?
Equivalence that is $$\forall_{x, y} ((\forall_z z\in x \iff z\in y)\iff x = y)$$ follows from logic. If $x, y$ are such that $x = y$, then given $z$, in the formula $z\in x$ we can substitute $x$ for $y$ to obtain $z\in y$. And conversely, we can substitute $y$ for $x$ in the formula $z\in y$ to obtain $z\in x$.
Wikipedia article says: "The converse, $\forall A \, \forall B \, (A = B \implies \forall X \, (X \in A \iff X \in B) )$, of this axiom follows from the substitution property of equality.
Equivalence that is $$\forall_{x, y} ((\forall_z z\in x \iff z\in y)\iff x = y)$$ follows from logic. If $x, y$ are such that $x = y$, then given $z$, in the formula $z\in x$ we can substitute $x$ for $y$ to obtain $z\in y$. And conversely, we can substitute $y$ for $x$ in the formula $z\in y$ to obtain $z\in x$.
Of course, if you meant formal proof in some deductive system (like Hilbert system or something similar), that would be more work.