Axiom ax-un

Description: Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states that a set y exists that includes the union of a given set x i.e. the collection of all members of the members of x . The variant axun2 states that the union itself exists. A version with the standard abbreviation for union is uniex2 . A version using class notation is uniex .

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

	Ref	Expression
Assertion	ax-un	$$⊢\exists y\forall z\left(\exists w\left(z\in w\wedge w\in x\right)\to z\in y\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	$$setvary$$
1		vz	$$setvarz$$
2		vw	$$setvarw$$
3	1	cv	$$setvarz$$
4	2	cv	$$setvarw$$
5	3 4	wcel	$$wffz\in w$$
6		vx	$$setvarx$$
7	6	cv	$$setvarx$$
8	4 7	wcel	$$wffw\in x$$
9	5 8	wa	$$wff\left(z\in w\wedge w\in x\right)$$
10	9 2	wex	$$wff\exists w\left(z\in w\wedge w\in x\right)$$
11	0	cv	$$setvary$$
12	3 11	wcel	$$wffz\in y$$
13	10 12	wi	$$wff\left(\exists w\left(z\in w\wedge w\in x\right)\to z\in y\right)$$
14	13 1	wal	$$wff\forall z\left(\exists w\left(z\in w\wedge w\in x\right)\to z\in y\right)$$
15	14 0	wex	$$wff\exists y\forall z\left(\exists w\left(z\in w\wedge w\in x\right)\to z\in y\right)$$