Metamath Proof Explorer


Theorem f1ocnvfv3

Description: Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion f1ocnvfv3 F : A 1-1 onto B C B F -1 C = ι x A | F x = C

Proof

Step Hyp Ref Expression
1 f1ocnvdm F : A 1-1 onto B C B F -1 C A
2 f1ocnvfvb F : A 1-1 onto B x A C B F x = C F -1 C = x
3 2 3expa F : A 1-1 onto B x A C B F x = C F -1 C = x
4 3 an32s F : A 1-1 onto B C B x A F x = C F -1 C = x
5 eqcom x = F -1 C F -1 C = x
6 4 5 bitr4di F : A 1-1 onto B C B x A F x = C x = F -1 C
7 1 6 riota5 F : A 1-1 onto B C B ι x A | F x = C = F -1 C
8 7 eqcomd F : A 1-1 onto B C B F -1 C = ι x A | F x = C