Metamath Proof Explorer

Theorem feq1

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

Ref Expression
Assertion feq1 ⊢ F = G → F : A ⟶ B ↔ G : A ⟶ B

Proof

Step Hyp Ref Expression
1 fneq1 ⊢ F = G → F Fn A ↔ G Fn A
2 rneq ⊢ F = G → ran ⁡ F = ran ⁡ G
3 2 sseq1d ⊢ F = G → ran ⁡ F ⊆ B ↔ ran ⁡ G ⊆ B
4 1 3 anbi12d ⊢ F = G → F Fn A ∧ ran ⁡ F ⊆ B ↔ G Fn A ∧ ran ⁡ G ⊆ B
5 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
6 df-f ⊢ G : A ⟶ B ↔ G Fn A ∧ ran ⁡ G ⊆ B
7 4 5 6 3bitr4g ⊢ F = G → F : A ⟶ B ↔ G : A ⟶ B