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

Definition df-ofr 6297
 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 6295 . 2
3 vx . . . . . . 7
43cv 1651 . . . . . 6
5 vf . . . . . . 7
65cv 1651 . . . . . 6
74, 6cfv 5445 . . . . 5
8 vg . . . . . . 7
98cv 1651 . . . . . 6
104, 9cfv 5445 . . . . 5
117, 10, 1wbr 4204 . . . 4
126cdm 4869 . . . . 5
139cdm 4869 . . . . 5
1412, 13cin 3311 . . . 4
1511, 3, 14wral 2697 . . 3
1615, 5, 8copab 4257 . 2
172, 16wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  ofreq  6299  ofrfval  6304
 Copyright terms: Public domain W3C validator