Metamath Proof Explorer

Theorem f1eq3

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997)

Ref Expression
Assertion f1eq3 ⊢A=B→F:C⟶1-1A↔F:C⟶1-1B

Proof

Step Hyp Ref Expression
1 feq3 ⊢A=B→F:C⟶A↔F:C⟶B
2 1 anbi1d ⊢A=B→F:C⟶A∧Fun⁡F-1↔F:C⟶B∧Fun⁡F-1
3 df-f1 ⊢F:C⟶1-1A↔F:C⟶A∧Fun⁡F-1
4 df-f1 ⊢F:C⟶1-1B↔F:C⟶B∧Fun⁡F-1
5 2 3 4 3bitr4g ⊢A=B→F:C⟶1-1A↔F:C⟶1-1B