Metamath Proof Explorer


Theorem f1ocnvfv

Description: Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Assertion f1ocnvfv F:A1-1 ontoBCAFC=DF-1D=C

Proof

Step Hyp Ref Expression
1 fveq2 D=FCF-1D=F-1FC
2 1 eqcoms FC=DF-1D=F-1FC
3 f1ocnvfv1 F:A1-1 ontoBCAF-1FC=C
4 3 eqeq2d F:A1-1 ontoBCAF-1D=F-1FCF-1D=C
5 2 4 syl5ib F:A1-1 ontoBCAFC=DF-1D=C