Definition df-uni 1920

Description: Define the union of a class. Definition 5.5 of [TakeutiZaring] p. 16.

Assertion

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

Distinct variable group(s):   x,y,A

Detailed syntax breakdown of Definition df-uni

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cuni 1919	. 2 class ∪A
3		vx	. . . . . 6 set x
4		vy	. . . . . 6 set y
5	3, 4	wel 803	. . . . 5 wff x ∈ y
6	4	cv 1089	. . . . . 6 class y
7	6, 1	wcel 1092	. . . . 5 wff y ∈ A
8	5, 7	wa 196	. . . 4 wff (x ∈ y ∧ y ∈ A)
9	8, 4	wex 678	. . 3 wff ∃y(x ∈ y ∧ y ∈ A)
10	9, 3	cab 1090	. 2 class {x∣∃y(x ∈ y ∧ y ∈ A)}
11	2, 10	wceq 1091	1 wff ∪A = {x∣∃y(x ∈ y ∧ y ∈ A)}

This definition is referenced by:  dfuni2 1921  eluni 1922  unieq 1927  unpr 1930  uniss 1936  dfiun2 2014

metamath.org