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?

@JuanJesús The axiom of extensionality you refer to states that $$\forall_{x, y} ((\forall_z z\in x \iff z\in y ) \implies x = y)$$

@JuanJesús I think the other implication follows from the axioms of formal logic. (Basically in any reasonable system you're using.)

If a=b, then formulas φ(a) and φ(b) are equivalent. (Here φ(a)≡z∈a.)

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.

@Jakobian Yes

@MartinSleziak Mmm, how can you use that principle to derive the contraposition of the axiom?

@JuanJesús Basically what I wrote above - and what Jakobian wrote in detail.

Of course, if you meant formal proof in some deductive system (like Hilbert system or something similar), that would be more work.