Theorem f1eq3

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

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

Proof

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