Axiom ax-ext 1074

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 this version of Extensionality with Metamath's logical axioms, on the other hand, we could delete from them ax-8 798 through ax-16 922, leaving only the beautifully simple ax-4 673 through ax-7 676 (and ax-gen 677), and those that we couldn't prove as theorems we would add back as additional axioms of set theory. Or should they still be considered part of "logic" proper? I suppose this is a philosophical issue. Under traditional predicate calculus, this version of Extensionality moves the properties of equality into set theory, and it can be argued that proper substitution - which is broken out explicitly in the Metamath axioms - has an intimate tie-in with equality that is implicitly "hidden" in the traditional axioms of predicate calculus. The axiomatics of such a system - i.e. devising simple, elegant axioms - have apparently never been studied nor even considered. (Perhaps some day I will play with it if no one else does.)

Assertion

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

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Axiom ax-ext

Step	Hyp	Ref	Expression
1		vz	. . . . 5 set z
2		vx	. . . . 5 set x
3	1, 2	wel 803	. . . 4 wff z e. x
4		vy	. . . . 5 set y
5	1, 4	wel 803	. . . 4 wff z e. y
6	3, 5	wb 127	. . 3 wff (z e. x <-> z e. y)
7	6, 1	wal 672	. 2 wff A.z(z e. x <-> z e. y)
8	2, 4	weq 797	. 2 wff x = y
9	7, 8	wi 2	1 wff (A.z(z e. x <-> z e. y) -> x = y)

This axiom is referenced by:  axext 1086  zfext2 1087  bm1.1 1088  dfcleq 1098

metamath.org