**Description:** Axiom of extensionality. An axiom of Zermelo-Fraenkel set theory. It
states that two sets are identical if they contain the same elements.
Axiom Ext of BellMachover p. 461. Its converse is a theorem of
predicate logic, elequ2g .

Set theory can also be formulated with a*single* primitive predicate
e. on top of traditional predicate calculus*without* equality. In
that case the Axiom of Extensionality becomes
( A. w ( w e. x <-> w e. y ) -> ( x e. z -> y e. z ) ) , and
equality x = y is*defined* as A. w ( w e. x <-> w e. y ) . All
of the usual axioms of equality then become theorems of set theory.
See, for example, Axiom 1 of TakeutiZaring p. 8.

To use the above "equality-free" version of Extensionality with Metamath's predicate calculus axioms, we would rewrite all axioms involving equality with equality expanded according to the above definition. Some of those axioms may be provable from ax-ext and would become redundant, but this hasn't been studied carefully.

*General remarks*: Our set theory axioms are presented using defined
connectives ( <-> , E. , etc.) for convenience. However, it is
implicitly understood that the actual axioms use only the primitive
connectives -> , -. , A. , = , and e. . It is
straightforward to establish the equivalence between the actual axioms
and the ones we display, and we will not do so.

It is important to understand that strictly speaking, all of our set
theory axioms are really schemes that represent an infinite number of
actual axioms. This is inherent in the design of Metamath
("metavariable math"), which manipulates only metavariables. For
example, the metavariable x in ax-ext can represent any actual
variable*v1*,*v2*,*v3*,... . Distinct variable restrictions ($d)
prevent us from substituting say*v1* for both x and z . This
is in contrast to typical textbook presentations that present actual
axioms (except for Replacement ax-rep , which involves a wff
metavariable). In practice, though, the theorems and proofs are
essentially the same. The $d restrictions make each of the infinite
axioms generated by the ax-ext scheme exactly logically equivalent to
each other and in particular to the actual axiom of the textbook
version. (Contributed by NM, 21-May-1993)

Ref | Expression | ||
---|---|---|---|

Assertion | ax-ext | $${\u22a2}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\leftrightarrow {z}\in {y}\right)\to {x}={y}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

0 | vz | $${setvar}{z}$$ | |

1 | 0 | cv | $${setvar}{z}$$ |

2 | vx | $${setvar}{x}$$ | |

3 | 2 | cv | $${setvar}{x}$$ |

4 | 1 3 | wcel | $${wff}{z}\in {x}$$ |

5 | vy | $${setvar}{y}$$ | |

6 | 5 | cv | $${setvar}{y}$$ |

7 | 1 6 | wcel | $${wff}{z}\in {y}$$ |

8 | 4 7 | wb | $${wff}\left({z}\in {x}\leftrightarrow {z}\in {y}\right)$$ |

9 | 8 0 | wal | $${wff}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\leftrightarrow {z}\in {y}\right)$$ |

10 | 3 6 | wceq | $${wff}{x}={y}$$ |

11 | 9 10 | wi | $${wff}\left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\leftrightarrow {z}\in {y}\right)\to {x}={y}\right)$$ |