Axiom ax-bj-bun 35708

Description: Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)

Assertion

Ref	Expression
ax-bj-bun	⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))

Distinct variable group:   𝑥,𝑦,𝑧,𝑡

Detailed syntax breakdown of Axiom ax-bj-bun

Step	Hyp	Ref	Expression
1		vt	. . . . . . 7 setvar 𝑡
2		vz	. . . . . . 7 setvar 𝑧
3	1, 2	wel 2107	. . . . . 6 wff 𝑡 ∈ 𝑧
4		vx	. . . . . . . 8 setvar 𝑥
5	1, 4	wel 2107	. . . . . . 7 wff 𝑡 ∈ 𝑥
6		vy	. . . . . . . 8 setvar 𝑦
7	1, 6	wel 2107	. . . . . . 7 wff 𝑡 ∈ 𝑦
8	5, 7	wo 845	. . . . . 6 wff (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)
9	3, 8	wb 205	. . . . 5 wff (𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
10	9, 1	wal 1539	. . . 4 wff ∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
11	10, 2	wex 1781	. . 3 wff ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
12	11, 6	wal 1539	. 2 wff ∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
13	12, 4	wal 1539	1 wff ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))

This axiom is referenced by:  bj-unexg  35709