# Metamath Proof Explorer

## Theorem f1oeq3

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

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

### Proof

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