Axiom ax-bj-bun

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

	Ref	Expression
Assertion	ax-bj-bun	|- A. x A. y E. z A. t ( t e. z <-> ( t e. x \/ t e. y ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		vy	|- y
2		vz	|- z
3		vt	|- t
4	3	cv	|- t
5	2	cv	|- z
6	4 5	wcel	|- t e. z
7	0	cv	|- x
8	4 7	wcel	|- t e. x
9	1	cv	|- y
10	4 9	wcel	|- t e. y
11	8 10	wo	|- ( t e. x \/ t e. y )
12	6 11	wb	|- ( t e. z <-> ( t e. x \/ t e. y ) )
13	12 3	wal	|- A. t ( t e. z <-> ( t e. x \/ t e. y ) )
14	13 2	wex	|- E. z A. t ( t e. z <-> ( t e. x \/ t e. y ) )
15	14 1	wal	|- A. y E. z A. t ( t e. z <-> ( t e. x \/ t e. y ) )
16	15 0	wal	|- A. x A. y E. z A. t ( t e. z <-> ( t e. x \/ t e. y ) )