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

Definition df-ofr 6309
 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 6307 . 2
3 vx . . . . . . 7
43cv 1652 . . . . . 6
5 vf . . . . . . 7
65cv 1652 . . . . . 6
74, 6cfv 5457 . . . . 5
8 vg . . . . . . 7
98cv 1652 . . . . . 6
104, 9cfv 5457 . . . . 5
117, 10, 1wbr 4215 . . . 4
126cdm 4881 . . . . 5
139cdm 4881 . . . . 5
1412, 13cin 3321 . . . 4
1511, 3, 14wral 2707 . . 3
1615, 5, 8copab 4268 . 2
172, 16wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  ofreq  6311  ofrfval  6316
 Copyright terms: Public domain W3C validator