# Metamath Proof Explorer

## Theorem f1oeq1

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

Ref Expression
Assertion f1oeq1 ${⊢}{F}={G}\to \left({F}:{A}\underset{1-1 onto}{⟶}{B}↔{G}:{A}\underset{1-1 onto}{⟶}{B}\right)$

### Proof

Step Hyp Ref Expression
1 f1eq1 ${⊢}{F}={G}\to \left({F}:{A}\underset{1-1}{⟶}{B}↔{G}:{A}\underset{1-1}{⟶}{B}\right)$
2 foeq1 ${⊢}{F}={G}\to \left({F}:{A}\underset{onto}{⟶}{B}↔{G}:{A}\underset{onto}{⟶}{B}\right)$
3 1 2 anbi12d ${⊢}{F}={G}\to \left(\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)↔\left({G}:{A}\underset{1-1}{⟶}{B}\wedge {G}:{A}\underset{onto}{⟶}{B}\right)\right)$
4 df-f1o ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)$
5 df-f1o ${⊢}{G}:{A}\underset{1-1 onto}{⟶}{B}↔\left({G}:{A}\underset{1-1}{⟶}{B}\wedge {G}:{A}\underset{onto}{⟶}{B}\right)$
6 3 4 5 3bitr4g ${⊢}{F}={G}\to \left({F}:{A}\underset{1-1 onto}{⟶}{B}↔{G}:{A}\underset{1-1 onto}{⟶}{B}\right)$