This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1oeq3dd

Description: Equality deduction for one-to-one onto functions. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses f1oeq3dd.1 ⊢ φ → F : C ⟶ 1-1 onto A
f1oeq3dd.2 ⊢ φ → A = B
Assertion f1oeq3dd ⊢ φ → F : C ⟶ 1-1 onto B

Proof

Step Hyp Ref Expression
1 f1oeq3dd.1 ⊢ φ → F : C ⟶ 1-1 onto A
2 f1oeq3dd.2 ⊢ φ → A = B
3 2 f1oeq3d ⊢ φ → F : C ⟶ 1-1 onto A ↔ F : C ⟶ 1-1 onto B
4 1 3 mpbid ⊢ φ → F : C ⟶ 1-1 onto B