Metamath Proof Explorer

Theorem foeq3

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

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

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ 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-fo ⊢ F : C ⟶ onto A ↔ F Fn C ∧ ran ⁡ F = A
4 df-fo ⊢ F : C ⟶ onto B ↔ F Fn C ∧ ran ⁡ F = B
5 2 3 4 3bitr4g ⊢ A = B → F : C ⟶ onto A ↔ F : C ⟶ onto B