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 F F 1 st X = 2 nd X

Proof

Step Hyp Ref Expression
1 funrel Fun F Rel F
2 1st2nd Rel F X F X = 1 st X 2 nd X
3 1 2 sylan Fun F X F X = 1 st X 2 nd X
4 eleq1 X = 1 st X 2 nd X X F 1 st X 2 nd X F
5 4 adantl Fun F X = 1 st X 2 nd X X F 1 st X 2 nd X F
6 funopfv Fun F 1 st X 2 nd X F F 1 st X = 2 nd X
7 6 adantr Fun F X = 1 st X 2 nd X 1 st X 2 nd X F F 1 st X = 2 nd X
8 5 7 sylbid Fun F X = 1 st X 2 nd X X F F 1 st X = 2 nd X
9 8 impancom Fun F X F X = 1 st X 2 nd X F 1 st X = 2 nd X
10 3 9 mpd Fun F X F F 1 st X = 2 nd X