NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-uni1 GIF version

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
StepHypRef Expression
1 cA . . 3 class A
21cuni1 4133 . 2 class 1A
3 c1c 4134 . . . 4 class 1c
41, 3cin 3208 . . 3 class (A ∩ 1c)
54cuni 3891 . 2 class (A ∩ 1c)
62, 5wceq 1642 1 wff 1A = (A ∩ 1c)
Colors of variables: wff setvar class
This definition is referenced by:  eluni1g  4172
  Copyright terms: Public domain W3C validator