Definition df-restrict 31978

Description: Define the restriction function. See brrestrict 32056 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

Step	Hyp	Ref	Expression
1		crestrict 31958	. 2 class Restrict
2		ccap 31954	. . 3 class Cap
3		c1st 7166	. . . 4 class 1st
4		ccart 31948	. . . . 5 class Cart
5		c2nd 7167	. . . . . 6 class 2nd
6		crange 31951	. . . . . . 7 class Range
7	6, 3	ccom 5118	. . . . . 6 class (Range o. 1st )
8	5, 7	ctxp 31937	. . . . 5 class ( 2nd (x) (Range o. 1st ) )
9	4, 8	ccom 5118	. . . 4 class (Cart o. ( 2nd (x) (Range o. 1st ) ) )
10	3, 9	ctxp 31937	. . 3 class ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) )
11	2, 10	ccom 5118	. 2 class (Cap o. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) )
12	1, 11	wceq 1483	1 wff Restrict = (Cap o. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) )

This definition is referenced by:  brrestrict  32056