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

Definition df-ofr 6529
 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 6527 . 2
3 vx . . . . . . 7
43cv 1442 . . . . . 6
5 vf . . . . . . 7
65cv 1442 . . . . . 6
74, 6cfv 5581 . . . . 5
8 vg . . . . . . 7
98cv 1442 . . . . . 6
104, 9cfv 5581 . . . . 5
117, 10, 1wbr 4401 . . . 4
126cdm 4833 . . . . 5
139cdm 4833 . . . . 5
1412, 13cin 3402 . . . 4
1511, 3, 14wral 2736 . . 3
1615, 5, 8copab 4459 . 2
172, 16wceq 1443 1
 Colors of variables: wff setvar class This definition is referenced by:  ofreq  6531  ofrfval  6536
 Copyright terms: Public domain W3C validator