Axiom ax-un 4556

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 4558 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4559. A version using class notation is uniex 4560.

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 4233), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 266).

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

Assertion

Ref	Expression
ax-un	⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-un

Step	Hyp	Ref	Expression
1		vz	. . . . . . 7 setvar 𝑧
2		vw	. . . . . . 7 setvar 𝑤
3	1, 2	wel 2206	. . . . . 6 wff 𝑧 ∈ 𝑤
4		vx	. . . . . . 7 setvar 𝑥
5	2, 4	wel 2206	. . . . . 6 wff 𝑤 ∈ 𝑥
6	3, 5	wa 104	. . . . 5 wff (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)
7	6, 2	wex 1541	. . . 4 wff ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)
8		vy	. . . . 5 setvar 𝑦
9	1, 8	wel 2206	. . . 4 wff 𝑧 ∈ 𝑦
10	7, 9	wi 4	. . 3 wff (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
11	10, 1	wal 1396	. 2 wff ∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
12	11, 8	wex 1541	1 wff ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

This axiom is referenced by:  zfun  4557  axun2  4558  bj-axun2  16702