Metamath Proof Explorer

Theorem foeq123d

Description: Equality deduction for onto functions. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses f1eq123d.1 ⊢ φ → F = G
f1eq123d.2 ⊢ φ → A = B
f1eq123d.3 ⊢ φ → C = D
Assertion foeq123d ⊢ φ → F : A ⟶ onto C ↔ G : B ⟶ onto D

Proof

Step Hyp Ref Expression
1 f1eq123d.1 ⊢ φ → F = G
2 f1eq123d.2 ⊢ φ → A = B
3 f1eq123d.3 ⊢ φ → C = D
4 foeq1 ⊢ F = G → F : A ⟶ onto C ↔ G : A ⟶ onto C
5 1 4 syl ⊢ φ → F : A ⟶ onto C ↔ G : A ⟶ onto C
6 foeq2 ⊢ A = B → G : A ⟶ onto C ↔ G : B ⟶ onto C
7 2 6 syl ⊢ φ → G : A ⟶ onto C ↔ G : B ⟶ onto C
8 foeq3 ⊢ C = D → G : B ⟶ onto C ↔ G : B ⟶ onto D
9 3 8 syl ⊢ φ → G : B ⟶ onto C ↔ G : B ⟶ onto D
10 5 7 9 3bitrd ⊢ φ → F : A ⟶ onto C ↔ G : B ⟶ onto D