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 : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) <-> C = D ) )

Step	Hyp	Ref	Expression
1		f1veqaeq	\|- ( ( F : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) )
2		fveq2	\|- ( C = D -> ( F ` C ) = ( F ` D ) )
3	1 2	impbid1	\|- ( ( F : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) <-> C = D ) )

Step

Hyp

Ref

Expression

 |-  ( ( F : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) )

 |-  ( C = D -> ( F ` C ) = ( F ` D ) )

1 2

 |-  ( ( F : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) <-> C = D ) )