Description: Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dffn5f.1 | |
|
Assertion | dffn5f | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dffn5f.1 | |
|
2 | dffn5 | |
|
3 | nfcv | |
|
4 | 1 3 | nffv | |
5 | nfcv | |
|
6 | fveq2 | |
|
7 | 4 5 6 | cbvmpt | |
8 | 7 | eqeq2i | |
9 | 2 8 | bitri | |