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 ( 𝑥 = 𝑦 ↔ ∀ 𝑧 ( 𝑧𝑥𝑧𝑦 ) )

Proof

Step Hyp Ref Expression
1 elequ2g ( 𝑥 = 𝑦 → ∀ 𝑧 ( 𝑧𝑥𝑧𝑦 ) )
2 axextg ( ∀ 𝑧 ( 𝑧𝑥𝑧𝑦 ) → 𝑥 = 𝑦 )
3 1 2 impbii ( 𝑥 = 𝑦 ↔ ∀ 𝑧 ( 𝑧𝑥𝑧𝑦 ) )