Metamath Proof Explorer


Theorem f1fveq

Description: Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997)

Ref Expression
Assertion f1fveq F:A1-1BCADAFC=FDC=D

Proof

Step Hyp Ref Expression
1 f1veqaeq F:A1-1BCADAFC=FDC=D
2 fveq2 C=DFC=FD
3 1 2 impbid1 F:A1-1BCADAFC=FDC=D