Metamath Proof Explorer

Theorem f1cnv

Description: The converse of an injective function is bijective. (Contributed by FL, 11-Nov-2011)

Ref Expression
Assertion f1cnv 
|- ( F : A -1-1-> B -> `' F : ran F -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 f1f1orn 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
2 f1ocnv 
 |-  ( F : A -1-1-onto-> ran F -> `' F : ran F -1-1-onto-> A )
3 1 2 syl 
 |-  ( F : A -1-1-> B -> `' F : ran F -1-1-onto-> A )