Description: A onetoone onto mapping is a relation. (Contributed by NM, 13Dec2003)
Ref  Expression  

Assertion  f1orel   ( F : A 11onto> B > Rel F ) 
Step  Hyp  Ref  Expression 

1  f1ofun   ( F : A 11onto> B > Fun F ) 

2  funrel   ( Fun F > Rel F ) 

3  1 2  syl   ( F : A 11onto> B > Rel F ) 