Metamath Proof Explorer


Theorem 2ndval

Description: The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion 2ndval 2 nd A = ran A

Proof

Step Hyp Ref Expression
1 sneq x = A x = A
2 1 rneqd x = A ran x = ran A
3 2 unieqd x = A ran x = ran A
4 df-2nd 2 nd = x V ran x
5 snex A V
6 5 rnex ran A V
7 6 uniex ran A V
8 3 4 7 fvmpt A V 2 nd A = ran A
9 fvprc ¬ A V 2 nd A =
10 snprc ¬ A V A =
11 10 biimpi ¬ A V A =
12 11 rneqd ¬ A V ran A = ran
13 rn0 ran =
14 12 13 eqtrdi ¬ A V ran A =
15 14 unieqd ¬ A V ran A =
16 uni0 =
17 15 16 eqtrdi ¬ A V ran A =
18 9 17 eqtr4d ¬ A V 2 nd A = ran A
19 8 18 pm2.61i 2 nd A = ran A