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 <-> A. z ( z e. x <-> z e. y ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ2g | |- ( x = y -> A. z ( z e. x <-> z e. y ) ) |
|
2 | axextg | |- ( A. z ( z e. x <-> z e. y ) -> x = y ) |
|
3 | 1 2 | impbii | |- ( x = y <-> A. z ( z e. x <-> z e. y ) ) |