Metamath Proof Explorer

Theorem feq2

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion feq2 ⊢ A = B → F : A ⟶ C ↔ F : B ⟶ C

Proof

Step Hyp Ref Expression
1 fneq2 ⊢ A = B → F Fn A ↔ F Fn B
2 1 anbi1d ⊢ A = B → F Fn A ∧ ran ⁡ F ⊆ C ↔ F Fn B ∧ ran ⁡ F ⊆ C
3 df-f ⊢ F : A ⟶ C ↔ F Fn A ∧ ran ⁡ F ⊆ C
4 df-f ⊢ F : B ⟶ C ↔ F Fn B ∧ ran ⁡ F ⊆ C
5 2 3 4 3bitr4g ⊢ A = B → F : A ⟶ C ↔ F : B ⟶ C