Metamath Proof Explorer

Theorem funfv1st2nd

Description: The function value for the first component of an ordered pair is the second component of the ordered pair. (Contributed by AV, 17-Oct-2023)

Ref Expression
Assertion funfv1st2nd 
|- ( ( Fun F /\ X e. F ) -> ( F ` ( 1st ` X ) ) = ( 2nd ` X ) )

Proof

Step Hyp Ref Expression
1 funrel 
 |-  ( Fun F -> Rel F )
2 1st2nd 
 |-  ( ( Rel F /\ X e. F ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
3 1 2 sylan 
 |-  ( ( Fun F /\ X e. F ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
4 eleq1 
 |-  ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( X e. F <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. F ) )
5 4 adantl 
 |-  ( ( Fun F /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) -> ( X e. F <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. F ) )
6 funopfv 
 |-  ( Fun F -> ( <. ( 1st ` X ) , ( 2nd ` X ) >. e. F -> ( F ` ( 1st ` X ) ) = ( 2nd ` X ) ) )
7 6 adantr 
 |-  ( ( Fun F /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) -> ( <. ( 1st ` X ) , ( 2nd ` X ) >. e. F -> ( F ` ( 1st ` X ) ) = ( 2nd ` X ) ) )
8 5 7 sylbid 
 |-  ( ( Fun F /\ X = <. ( 1st ` X ) , ( 2nd ` X ) >. ) -> ( X e. F -> ( F ` ( 1st ` X ) ) = ( 2nd ` X ) ) )
9 8 impancom 
 |-  ( ( Fun F /\ X e. F ) -> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. -> ( F ` ( 1st ` X ) ) = ( 2nd ` X ) ) )
10 3 9 mpd 
 |-  ( ( Fun F /\ X e. F ) -> ( F ` ( 1st ` X ) ) = ( 2nd ` X ) )