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 )