Metamath Proof Explorer

Theorem feq123

Description: Equality theorem for functions. (Contributed by FL, 16-Nov-2008)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F = G /\ A = C /\ B = D ) -> F = G )
2 simp2 
 |-  ( ( F = G /\ A = C /\ B = D ) -> A = C )
3 simp3 
 |-  ( ( F = G /\ A = C /\ B = D ) -> B = D )
4 1 2 3 feq123d 
 |-  ( ( F = G /\ A = C /\ B = D ) -> ( F : A --> B <-> G : C --> D ) )