Metamath Proof Explorer

Theorem f1oeq123d

Description: Equality deduction for one-to-one 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 f1oeq123d ⊢ φ → F : A ⟶ 1-1 onto C ↔ G : B ⟶ 1-1 onto D

Proof

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