Definition df-uni1 4139

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 4174 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 4134	. 2 class ⋃1A
3		c1c 4135	. . . 4 class 1c
4	1, 3	cin 3209	. . 3 class (A ∩ 1c)
5	4	cuni 3892	. 2 class ∪(A ∩ 1c)
6	2, 5	wceq 1642	1 wff ⋃1A = ∪(A ∩ 1c)

This definition is referenced by:  eluni1g  4173