Definition df-uni1 4138

Description: Define the unit union of a class. This operation is used implicitly in both Holmes and Hailperin to complete their stratification algorithms, although neither provide explicit notation for it. See eluni1 4173 for membership condition. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-uni1	⊢ ⋃1A = ∪(A ∩ 1c)

Detailed syntax breakdown of Definition df-uni1

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cuni1 4133	. 2 class ⋃1A
3		c1c 4134	. . . 4 class 1c
4	1, 3	cin 3208	. . 3 class (A ∩ 1c)
5	4	cuni 3891	. 2 class ∪(A ∩ 1c)
6	2, 5	wceq 1642	1 wff ⋃1A = ∪(A ∩ 1c)

This definition is referenced by:  eluni1g  4172