MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-ext Structured version   Visualization version   GIF version

Axiom ax-ext 2751
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 on top of traditional predicate calculus without equality. In that case the Axiom of Extensionality becomes (∀𝑤(𝑤𝑥𝑤𝑦) → (𝑥𝑧𝑦𝑧)), and equality 𝑥 = 𝑦 is defined as 𝑤(𝑤𝑥𝑤𝑦). 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 (, , etc.) for convenience. However, it is implicitly understood that the actual axioms use only the primitive connectives , ¬, , =, and . 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 𝑥 in ax-ext 2751 can represent any actual variable v1, v2, v3,... . Distinct variable restrictions ($d) prevent us from substituting say v1 for both 𝑥 and 𝑧. This is in contrast to typical textbook presentations that present actual axioms (except for Replacement ax-rep 4905, 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 2751 scheme exactly logically equivalent to each other and in particular to the actual axiom of the textbook version. (Contributed by NM, 21-May-1993.)

Assertion
Ref Expression
ax-ext (∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-ext
StepHypRef Expression
1 vz . . . . 5 setvar 𝑧
2 vx . . . . 5 setvar 𝑥
31, 2wel 2146 . . . 4 wff 𝑧𝑥
4 vy . . . . 5 setvar 𝑦
51, 4wel 2146 . . . 4 wff 𝑧𝑦
63, 5wb 196 . . 3 wff (𝑧𝑥𝑧𝑦)
76, 1wal 1629 . 2 wff 𝑧(𝑧𝑥𝑧𝑦)
82, 4weq 2043 . 2 wff 𝑥 = 𝑦
97, 8wi 4 1 wff (∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
Colors of variables: wff setvar class
This axiom is referenced by:  axext2  2752  axext3  2753  axext3ALT  2754  bm1.1  2756  ax6vsep  4920  nfnid  5026  bj-axext3  33104  bj-ax9  33218  bj-ax9-2  33219  axc11next  39133
  Copyright terms: Public domain W3C validator