Metamath Proof Explorer
Description: A onetoone onto mapping is function on its domain. (Contributed by NM, 12Dec2003)


Ref 
Expression 

Assertion 
f1ofn 
$${\u22a2}{F}:{A}\underset{11\; onto}{\u27f6}{B}\to {F}Fn{A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

f1of 
$${\u22a2}{F}:{A}\underset{11\; onto}{\u27f6}{B}\to {F}:{A}\u27f6{B}$$ 
2 
1

ffnd 
$${\u22a2}{F}:{A}\underset{11\; onto}{\u27f6}{B}\to {F}Fn{A}$$ 