NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-uni1 Unicode 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 1 1c

Detailed syntax breakdown of Definition df-uni1
StepHypRef Expression
1 cA . . 3
21cuni1 4133 . 2 1
3 c1c 4134 . . . 4 1c
41, 3cin 3208 . . 3 1c
54cuni 3891 . 2 1c
62, 5wceq 1642 1 1 1c
Colors of variables: wff setvar class
This definition is referenced by:  eluni1g  4172
  Copyright terms: Public domain W3C validator