Metamath Proof Explorer


Theorem 2ndval2

Description: Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

Ref Expression
Assertion 2ndval2 A V × V 2 nd A = A -1

Proof

Step Hyp Ref Expression
1 elvv A V × V x y A = x y
2 vex x V
3 vex y V
4 2 3 op2nd 2 nd x y = y
5 2 3 op2ndb x y -1 = y
6 4 5 eqtr4i 2 nd x y = x y -1
7 fveq2 A = x y 2 nd A = 2 nd x y
8 sneq A = x y A = x y
9 8 cnveqd A = x y A -1 = x y -1
10 9 inteqd A = x y A -1 = x y -1
11 10 inteqd A = x y A -1 = x y -1
12 11 inteqd A = x y A -1 = x y -1
13 6 7 12 3eqtr4a A = x y 2 nd A = A -1
14 13 exlimivv x y A = x y 2 nd A = A -1
15 1 14 sylbi A V × V 2 nd A = A -1