![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-un | GIF version |
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 4460 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 4461. A version using class
notation is uniex 4462.
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 4146), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 266). The union of a class df-uni 3832 should not be confused with the union of two classes df-un 3153. Their relationship is shown in unipr 3845. (Contributed by NM, 23-Dec-1993.) |
Ref | Expression |
---|---|
ax-un | ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vz | . . . . . . 7 setvar 𝑧 | |
2 | vw | . . . . . . 7 setvar 𝑤 | |
3 | 1, 2 | wel 2161 | . . . . . 6 wff 𝑧 ∈ 𝑤 |
4 | vx | . . . . . . 7 setvar 𝑥 | |
5 | 2, 4 | wel 2161 | . . . . . 6 wff 𝑤 ∈ 𝑥 |
6 | 3, 5 | wa 104 | . . . . 5 wff (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) |
7 | 6, 2 | wex 1503 | . . . 4 wff ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) |
8 | vy | . . . . 5 setvar 𝑦 | |
9 | 1, 8 | wel 2161 | . . . 4 wff 𝑧 ∈ 𝑦 |
10 | 7, 9 | wi 4 | . . 3 wff (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
11 | 10, 1 | wal 1362 | . 2 wff ∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
12 | 11, 8 | wex 1503 | 1 wff ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) |
Colors of variables: wff set class |
This axiom is referenced by: zfun 4459 axun2 4460 bj-axun2 15331 |
Copyright terms: Public domain | W3C validator |