Theorem f1eq2

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997)

	Ref	Expression
Assertion	f1eq2	|- ( A = B -> ( F : A -1-1-> C <-> F : B -1-1-> C ) )

Proof

Step	Hyp	Ref	Expression
1		feq2	|- ( A = B -> ( F : A --> C <-> F : B --> C ) )
2	1	anbi1d	|- ( A = B -> ( ( F : A --> C /\ Fun `' F ) <-> ( F : B --> C /\ Fun `' F ) ) )
3		df-f1	|- ( F : A -1-1-> C <-> ( F : A --> C /\ Fun `' F ) )
4		df-f1	|- ( F : B -1-1-> C <-> ( F : B --> C /\ Fun `' F ) )
5	2 3 4	3bitr4g	|- ( A = B -> ( F : A -1-1-> C <-> F : B -1-1-> C ) )