# Metamath Proof Explorer

## Definition df-f1

Description: Define a one-to-one function. For equivalent definitions see dff12 and dff13 . Compare Definition 6.15(5) of TakeutiZaring p. 27. We use their notation ("1-1" above the arrow).

A one-to-one function is also called an "injection" or an "injective function", F : A -1-1-> B can be read as " F is an injection from A into B ". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon . (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion df-f1 ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cF ${class}{F}$
1 cA ${class}{A}$
2 cB ${class}{B}$
3 1 2 0 wf1 ${wff}{F}:{A}\underset{1-1}{⟶}{B}$
4 1 2 0 wf ${wff}{F}:{A}⟶{B}$
5 0 ccnv ${class}{{F}}^{-1}$
6 5 wfun ${wff}\mathrm{Fun}{{F}}^{-1}$
7 4 6 wa ${wff}\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
8 3 7 wb ${wff}\left({F}:{A}\underset{1-1}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)\right)$