Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-restrict Unicode version

Definition df-restrict 24412
Description: Define the restriction function. See brrestrict 24487 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
Assertion
Ref Expression
df-restrict  |- Restrict  =  (Cap 
o.  ( 1st  (x)  (Cart  o.  ( 2nd  (x)  (Range  o.  1st ) ) ) ) )

Detailed syntax breakdown of Definition df-restrict
StepHypRef Expression
1 crestrict 24394 . 2  class Restrict
2 ccap 24390 . . 3  class Cap
3 c1st 6120 . . . 4  class  1st
4 ccart 24384 . . . . 5  class Cart
5 c2nd 6121 . . . . . 6  class  2nd
6 crange 24387 . . . . . . 7  class Range
76, 3ccom 4693 . . . . . 6  class  (Range  o.  1st )
85, 7ctxp 24373 . . . . 5  class  ( 2nd  (x)  (Range  o.  1st )
)
94, 8ccom 4693 . . . 4  class  (Cart  o.  ( 2nd  (x)  (Range  o.  1st ) ) )
103, 9ctxp 24373 . . 3  class  ( 1st  (x)  (Cart  o.  ( 2nd  (x)  (Range  o.  1st )
) ) )
112, 10ccom 4693 . 2  class  (Cap  o.  ( 1st  (x)  (Cart  o.  ( 2nd  (x)  (Range  o.  1st ) ) ) ) )
121, 11wceq 1623 1  wff Restrict  =  (Cap 
o.  ( 1st  (x)  (Cart  o.  ( 2nd  (x)  (Range  o.  1st ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  brrestrict  24487
  Copyright terms: Public domain W3C validator