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	|- ( 2nd ` A ) = U. 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 -> U. ran { x } = U. ran { A } )
4		df-2nd	|- 2nd = ( x e. _V |-> U. ran { x } )
5		snex	|- { A } e. _V
6	5	rnex	|- ran { A } e. _V
7	6	uniex	|- U. ran { A } e. _V
8	3 4 7	fvmpt	|- ( A e. _V -> ( 2nd ` A ) = U. ran { A } )
9		fvprc	|- ( -. A e. _V -> ( 2nd ` A ) = (/) )
10		snprc	|- ( -. A e. _V <-> { A } = (/) )
11	10	biimpi	|- ( -. A e. _V -> { A } = (/) )
12	11	rneqd	|- ( -. A e. _V -> ran { A } = ran (/) )
13		rn0	|- ran (/) = (/)
14	12 13	eqtrdi	|- ( -. A e. _V -> ran { A } = (/) )
15	14	unieqd	|- ( -. A e. _V -> U. ran { A } = U. (/) )
16		uni0	|- U. (/) = (/)
17	15 16	eqtrdi	|- ( -. A e. _V -> U. ran { A } = (/) )
18	9 17	eqtr4d	|- ( -. A e. _V -> ( 2nd ` A ) = U. ran { A } )
19	8 18	pm2.61i	|- ( 2nd ` A ) = U. ran { A }