Metamath Proof Explorer

Theorem f1orel

Description: A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003)

Ref Expression
Assertion f1orel 
|- ( F : A -1-1-onto-> B -> Rel F )

Proof

Step Hyp Ref Expression
1 f1ofun 
 |-  ( F : A -1-1-onto-> B -> Fun F )
2 funrel 
 |-  ( Fun F -> Rel F )
3 1 2 syl 
 |-  ( F : A -1-1-onto-> B -> Rel F )