Metamath Proof Explorer

Theorem foeq1

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

Ref Expression
Assertion foeq1 ⊢ F = G → F : A ⟶ onto B ↔ G : A ⟶ onto 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 eqeq1d ⊢ 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-fo ⊢ F : A ⟶ onto B ↔ F Fn A ∧ ran ⁡ F = B
6 df-fo ⊢ G : A ⟶ onto B ↔ G Fn A ∧ ran ⁡ G = B
7 4 5 6 3bitr4g ⊢ F = G → F : A ⟶ onto B ↔ G : A ⟶ onto B