Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ofr | Unicode version |
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.) |
Ref | Expression |
---|---|
df-ofr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cR | . . 3 | |
2 | 1 | cofr 5981 | . 2 |
3 | vx | . . . . . . 7 | |
4 | 3 | cv 1330 | . . . . . 6 |
5 | vf | . . . . . . 7 | |
6 | 5 | cv 1330 | . . . . . 6 |
7 | 4, 6 | cfv 5123 | . . . . 5 |
8 | vg | . . . . . . 7 | |
9 | 8 | cv 1330 | . . . . . 6 |
10 | 4, 9 | cfv 5123 | . . . . 5 |
11 | 7, 10, 1 | wbr 3929 | . . . 4 |
12 | 6 | cdm 4539 | . . . . 5 |
13 | 9 | cdm 4539 | . . . . 5 |
14 | 12, 13 | cin 3070 | . . . 4 |
15 | 11, 3, 14 | wral 2416 | . . 3 |
16 | 15, 5, 8 | copab 3988 | . 2 |
17 | 2, 16 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: ofreq 5985 nfofr 5988 ofrfval 5990 |
Copyright terms: Public domain | W3C validator |