ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-un GIF version

Axiom ax-un 4271
Description: Axiom of Union. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set 𝑦 exists that includes the union of a given set 𝑥 i.e. the collection of all members of the members of 𝑥. The variant axun2 4273 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4274. A version using class notation is uniex 4275.

This is Axiom 3 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3968), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 263).

The union of a class df-uni 3662 should not be confused with the union of two classes df-un 3006. Their relationship is shown in unipr 3675. (Contributed by NM, 23-Dec-1993.)

Assertion
Ref Expression
ax-un 𝑦𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-un
StepHypRef Expression
1 vz . . . . . . 7 setvar 𝑧
2 vw . . . . . . 7 setvar 𝑤
31, 2wel 1440 . . . . . 6 wff 𝑧𝑤
4 vx . . . . . . 7 setvar 𝑥
52, 4wel 1440 . . . . . 6 wff 𝑤𝑥
63, 5wa 103 . . . . 5 wff (𝑧𝑤𝑤𝑥)
76, 2wex 1427 . . . 4 wff 𝑤(𝑧𝑤𝑤𝑥)
8 vy . . . . 5 setvar 𝑦
91, 8wel 1440 . . . 4 wff 𝑧𝑦
107, 9wi 4 . . 3 wff (∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
1110, 1wal 1288 . 2 wff 𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
1211, 8wex 1427 1 wff 𝑦𝑧(∃𝑤(𝑧𝑤𝑤𝑥) → 𝑧𝑦)
Colors of variables: wff set class
This axiom is referenced by:  zfun  4272  axun2  4273  bj-axun2  12110
  Copyright terms: Public domain W3C validator