Metamath Proof Explorer


Theorem dffn5f

Description: Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypothesis dffn5f.1 _xF
Assertion dffn5f FFnAF=xAFx

Proof

Step Hyp Ref Expression
1 dffn5f.1 _xF
2 dffn5 FFnAF=zAFz
3 nfcv _xz
4 1 3 nffv _xFz
5 nfcv _zFx
6 fveq2 z=xFz=Fx
7 4 5 6 cbvmpt zAFz=xAFx
8 7 eqeq2i F=zAFzF=xAFx
9 2 8 bitri FFnAF=xAFx