Metamath Proof Explorer

Theorem feq23

Description: Equality theorem for functions. (Contributed by FL, 14-Jul-2007) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion feq23 
|- ( ( A = C /\ B = D ) -> ( F : A --> B <-> F : C --> D ) )

Proof

Step Hyp Ref Expression
1 feq2 
 |-  ( A = C -> ( F : A --> B <-> F : C --> B ) )
2 feq3 
 |-  ( B = D -> ( F : C --> B <-> F : C --> D ) )
3 1 2 sylan9bb 
 |-  ( ( A = C /\ B = D ) -> ( F : A --> B <-> F : C --> D ) )