Definition df-ofr 6062

Description: Define the function relation map. The definition is designed so that if R is a binary relation, then oF R is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014.)

Assertion

Ref	Expression
df-ofr	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }

Distinct variable group:   f, g, x, R

Detailed syntax breakdown of Definition df-ofr

Step	Hyp	Ref	Expression
1		cR	. . 3 class R
2	1	cofr 6060	. 2 class oR R
3		vx	. . . . . . 7 setvar x
4	3	cv 1347	. . . . . 6 class x
5		vf	. . . . . . 7 setvar f
6	5	cv 1347	. . . . . 6 class f
7	4, 6	cfv 5198	. . . . 5 class ( f ` x )
8		vg	. . . . . . 7 setvar g
9	8	cv 1347	. . . . . 6 class g
10	4, 9	cfv 5198	. . . . 5 class ( g ` x )
11	7, 10, 1	wbr 3989	. . . 4 wff ( f ` x ) R ( g ` x )
12	6	cdm 4611	. . . . 5 class dom f
13	9	cdm 4611	. . . . 5 class dom g
14	12, 13	cin 3120	. . . 4 class ( dom f i^i dom g )
15	11, 3, 14	wral 2448	. . 3 wff A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x )
16	15, 5, 8	copab 4049	. 2 class { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
17	2, 16	wceq 1348	1 wff oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }

This definition is referenced by:  ofreq  6064  nfofr  6067  ofrfval  6069