MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ofr Unicode version

Definition df-ofr 6541
Description: Define the function relation map. The definition is designed so that if is a binary relation, then 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
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-ofr
StepHypRef Expression
1 cR . . 3
21cofr 6539 . 2
3 vx . . . . . . 7
43cv 1394 . . . . . 6
5 vf . . . . . . 7
65cv 1394 . . . . . 6
74, 6cfv 5593 . . . . 5
8 vg . . . . . . 7
98cv 1394 . . . . . 6
104, 9cfv 5593 . . . . 5
117, 10, 1wbr 4452 . . . 4
126cdm 5004 . . . . 5
139cdm 5004 . . . . 5
1412, 13cin 3474 . . . 4
1511, 3, 14wral 2807 . . 3
1615, 5, 8copab 4509 . 2
172, 16wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  ofreq  6543  ofrfval  6548
  Copyright terms: Public domain W3C validator