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

Definition df-ofr 6041
 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 6039 . 2
3 vx . . . . . . 7
43cv 1623 . . . . . 6
5 vf . . . . . . 7
65cv 1623 . . . . . 6
74, 6cfv 5222 . . . . 5
8 vg . . . . . . 7
98cv 1623 . . . . . 6
104, 9cfv 5222 . . . . 5
117, 10, 1wbr 4025 . . . 4
126cdm 4689 . . . . 5
139cdm 4689 . . . . 5
1412, 13cin 3153 . . . 4
1511, 3, 14wral 2545 . . 3
1615, 5, 8copab 4078 . 2
172, 16wceq 1624 1
 Colors of variables: wff set class This definition is referenced by:  ofreq  6043  nfofr  6046  ofrfval  6048
 Copyright terms: Public domain W3C validator