Metamath Proof Explorer

Theorem feq3

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

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

Proof

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