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

Axiom ax-un 4136
 Description: Axiom of Union. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set y exists that includes the union of a given set x i.e. the collection of all members of the members of x. The variant axun2 4138 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4139. A version using class notation is uniex 4140. 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 3869), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 253). The union of a class df-uni 3572 should not be confused with the union of two classes df-un 2916. Their relationship is shown in unipr 3585. (Contributed by NM, 23-Dec-1993.)
Assertion
Ref Expression
ax-un yz(w(z w w x) → z y)
Distinct variable group:   x,w,y,z

Detailed syntax breakdown of Axiom ax-un
StepHypRef Expression
1 vz . . . . . . 7 setvar z
2 vw . . . . . . 7 setvar w
31, 2wel 1391 . . . . . 6 wff z w
4 vx . . . . . . 7 setvar x
52, 4wel 1391 . . . . . 6 wff w x
63, 5wa 97 . . . . 5 wff (z w w x)
76, 2wex 1378 . . . 4 wff w(z w w x)
8 vy . . . . 5 setvar y
91, 8wel 1391 . . . 4 wff z y
107, 9wi 4 . . 3 wff (w(z w w x) → z y)
1110, 1wal 1240 . 2 wff z(w(z w w x) → z y)
1211, 8wex 1378 1 wff yz(w(z w w x) → z y)
 Colors of variables: wff set class This axiom is referenced by:  zfun  4137  axun2  4138  bj-axun2  9346
 Copyright terms: Public domain W3C validator