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 e. B ) -> ( `' F ` C ) = ( iota_ x e. A ( F ` x ) = C ) )

Proof

Step Hyp Ref Expression
1 f1ocnvdm 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( `' F ` C ) e. A )
2 f1ocnvfvb 
 |-  ( ( F : A -1-1-onto-> B /\ x e. A /\ C e. B ) -> ( ( F ` x ) = C <-> ( `' F ` C ) = x ) )
3 2 3expa 
 |-  ( ( ( F : A -1-1-onto-> B /\ x e. A ) /\ C e. B ) -> ( ( F ` x ) = C <-> ( `' F ` C ) = x ) )
4 3 an32s 
 |-  ( ( ( F : A -1-1-onto-> B /\ C e. B ) /\ x e. A ) -> ( ( F ` x ) = C <-> ( `' F ` C ) = x ) )
5 eqcom 
 |-  ( x = ( `' F ` C ) <-> ( `' F ` C ) = x )
6 4 5 bitr4di 
 |-  ( ( ( F : A -1-1-onto-> B /\ C e. B ) /\ x e. A ) -> ( ( F ` x ) = C <-> x = ( `' F ` C ) ) )
7 1 6 riota5 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( iota_ x e. A ( F ` x ) = C ) = ( `' F ` C ) )
8 7 eqcomd 
 |-  ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( `' F ` C ) = ( iota_ x e. A ( F ` x ) = C ) )