Axiom ax-ext 1702

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.

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 logical axioms, we would rewrite ax-8 1144 through ax-16 1418 with equality expanded according to the above definition. Some of those axioms could be proved from set theory and would be redundant. Not all of them are redundant, since our axioms of predicate calculus make essential use of equality for the proper substitution that is a primitive notion in traditional predicate calculus. A study of such an axiomatization would be an interesting project for someone exploring the foundations of logic.

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 1702 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 3243, which involves a wff metavariable). In practice, though, the theorems and proofs are essentially the same. The $d restrictions make each of the the infinite axioms generated by the ax-ext 1702 scheme exactly logically equivalent to each other and in particular to the actual axiom of the textbook version.

Assertion

Ref	Expression
ax-ext	|- (A.z(z e. x <-> z e. y) -> x = y)

Distinct variable group:   x,y,z

Detailed syntax breakdown of Axiom ax-ext

Step	Hyp	Ref	Expression
1		vz	. . . . . 6 set z
2	1	cv 1135	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 1135	. . . . 5 class x
5	2, 4	wcel 1138	. . . 4 wff z e. x
6		vy	. . . . . 6 set y
7	6	cv 1135	. . . . 5 class y
8	2, 7	wcel 1138	. . . 4 wff z e. y
9	5, 8	wb 162	. . 3 wff (z e. x <-> z e. y)
10	9, 1	wal 1134	. 2 wff A.z(z e. x <-> z e. y)
11	4, 7	wceq 1136	. 2 wff x = y
12	10, 11	wi 3	1 wff (A.z(z e. x <-> z e. y) -> x = y)

This axiom is referenced by:  axext2 1703  axext3 1704  axext3OLD 1705  bm1.1 1707  dfcleq 1715  ax10ext 16046

Copyright terms: Public domain