Theorem feq23i

Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Hypotheses	feq23i.1	|- A = C
	feq23i.2	|- B = D
Assertion	feq23i	|- ( F : A --> B <-> F : C --> D )

Proof

Step	Hyp	Ref	Expression
1		feq23i.1	|- A = C
2		feq23i.2	|- B = D
3		feq23	|- ( ( A = C /\ B = D ) -> ( F : A --> B <-> F : C --> D ) )
4	1 2 3	mp2an	|- ( F : A --> B <-> F : C --> D )