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 C_ a /\ (R"a) C_ a)}

Distinct variable groups:   S,a   R,a

Detailed syntax breakdown of Definition df-clos1

Step	Hyp	Ref	Expression
1		cS	. . 3 class S
2		cR	. . 3 class R
3	1, 2	cclos1 5872	. 2 class Clos1 (S, R)
4		va	. . . . . . 7 setvar a
5	4	cv 1641	. . . . . 6 class a
6	1, 5	wss 3257	. . . . 5 wff S C_ a
7	2, 5	cima 4722	. . . . . 6 class (R"a)
8	7, 5	wss 3257	. . . . 5 wff (R"a) C_ a
9	6, 8	wa 358	. . . 4 wff (S C_ a /\ (R"a) C_ a)
10	9, 4	cab 2339	. . 3 class {a | (S C_ a /\ (R"a) C_ a)}
11	10	cint 3926	. 2 class |^|{a | (S C_ a /\ (R"a) C_ a)}
12	3, 11	wceq 1642	1 wff Clos1 (S, R) = |^|{a | (S C_ a /\ (R"a) C_ a)}

This definition is referenced by:  clos1eq1  5874  clos1eq2  5875  clos1ex  5876  clos1base  5878  clos1conn  5879  clos1induct  5880  dfnnc3  5885  nchoicelem10  6296