This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axextb

Description: A bidirectional version of the axiom of extensionality. Although this theorem looks like a definition of equality, it requires the axiom of extensionality for its proof under our axiomatization. See the comments for ax-ext and df-cleq . (Contributed by NM, 14-Nov-2008)

Ref Expression
Assertion axextb ⊢ x = y ↔ ∀ z z ∈ x ↔ z ∈ y

Proof

Step Hyp Ref Expression
1 elequ2g ⊢ x = y → ∀ z z ∈ x ↔ z ∈ y
2 axextg ⊢ ∀ z z ∈ x ↔ z ∈ y → x = y
3 1 2 impbii ⊢ x = y ↔ ∀ z z ∈ x ↔ z ∈ y