Axiom ax-bj-bun

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

	Ref	Expression
Assertion	ax-bj-bun	$$⊢\forall x\forall y\exists z\forall t\left(t\in z\leftrightarrow \left(t\in x\vee t\in y\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		vy	$$setvary$$
2		vz	$$setvarz$$
3		vt	$$setvart$$
4	3	cv	$$setvart$$
5	2	cv	$$setvarz$$
6	4 5	wcel	$$wfft\in z$$
7	0	cv	$$setvarx$$
8	4 7	wcel	$$wfft\in x$$
9	1	cv	$$setvary$$
10	4 9	wcel	$$wfft\in y$$
11	8 10	wo	$$wff\left(t\in x\vee t\in y\right)$$
12	6 11	wb	$$wff\left(t\in z\leftrightarrow \left(t\in x\vee t\in y\right)\right)$$
13	12 3	wal	$$wff\forall t\left(t\in z\leftrightarrow \left(t\in x\vee t\in y\right)\right)$$
14	13 2	wex	$$wff\exists z\forall t\left(t\in z\leftrightarrow \left(t\in x\vee t\in y\right)\right)$$
15	14 1	wal	$$wff\forall y\exists z\forall t\left(t\in z\leftrightarrow \left(t\in x\vee t\in y\right)\right)$$
16	15 0	wal	$$wff\forall x\forall y\exists z\forall t\left(t\in z\leftrightarrow \left(t\in x\vee t\in y\right)\right)$$