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

Definition df-clos1 5873
Description: Define the closure operation. A modified version of the definition from [Rosser] p. 245. (Contributed by SF, 11-Feb-2015.)
Assertion
Ref Expression
df-clos1 Clos1 (S, R) = {a (S a (Ra) a)}
Distinct variable groups:   S,a   R,a

Detailed syntax breakdown of Definition df-clos1
StepHypRef Expression
1 cS . . 3 class S
2 cR . . 3 class R
31, 2cclos1 5872 . 2 class Clos1 (S, R)
4 va . . . . . . 7 setvar a
54cv 1641 . . . . . 6 class a
61, 5wss 3257 . . . . 5 wff S a
72, 5cima 4722 . . . . . 6 class (Ra)
87, 5wss 3257 . . . . 5 wff (Ra) a
96, 8wa 358 . . . 4 wff (S a (Ra) a)
109, 4cab 2339 . . 3 class {a (S a (Ra) a)}
1110cint 3926 . 2 class {a (S a (Ra) a)}
123, 11wceq 1642 1 wff Clos1 (S, R) = {a (S a (Ra) a)}
Colors of variables: wff setvar class
This definition is referenced by:  clos1eq1  5874  clos1eq2  5875  clos1ex  5876  clos1base  5878  clos1conn  5879  clos1induct  5880  dfnnc3  5885  nchoicelem10  6296
  Copyright terms: Public domain W3C validator