Definition df-uni 2570

Description: Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16.

Assertion

Ref	Expression
df-uni	⊢ ∪A = {x∣∃y(x ∈ y ⋀ y ∈ A)}

Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-uni

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cuni 2569	. 2 class ∪A
3		vx	. . . . . . 7 set x
4	3	cv 991	. . . . . 6 class x
5		vy	. . . . . . 7 set y
6	5	cv 991	. . . . . 6 class y
7	4, 6	wcel 994	. . . . 5 wff x ∈ y
8	6, 1	wcel 994	. . . . 5 wff y ∈ A
9	7, 8	wa 221	. . . 4 wff (x ∈ y ⋀ y ∈ A)
10	9, 5	wex 1016	. . 3 wff ∃y(x ∈ y ⋀ y ∈ A)
11	10, 3	cab 1505	. 2 class {x∣∃y(x ∈ y ⋀ y ∈ A)}
12	2, 11	wceq 992	1 wff ∪A = {x∣∃y(x ∈ y ⋀ y ∈ A)}

This definition is referenced by:  dfuni2 2571  eluni 2572  unieq 2576  unipr 2581  uniss 2588  dfiun2g 2654  uniuni 3104

Copyright terms: Public domain