Theorem 1stval

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

	Ref	Expression
Assertion	1stval	|- ( 1st ` A ) = U. dom { A }

Proof

Step	Hyp	Ref	Expression
1		sneq	|- ( x = A -> { x } = { A } )
2	1	dmeqd	|- ( x = A -> dom { x } = dom { A } )
3	2	unieqd	|- ( x = A -> U. dom { x } = U. dom { A } )
4		df-1st	|- 1st = ( x e. _V |-> U. dom { x } )
5		snex	|- { A } e. _V
6	5	dmex	|- dom { A } e. _V
7	6	uniex	|- U. dom { A } e. _V
8	3 4 7	fvmpt	|- ( A e. _V -> ( 1st ` A ) = U. dom { A } )
9		fvprc	|- ( -. A e. _V -> ( 1st ` A ) = (/) )
10		snprc	|- ( -. A e. _V <-> { A } = (/) )
11	10	biimpi	|- ( -. A e. _V -> { A } = (/) )
12	11	dmeqd	|- ( -. A e. _V -> dom { A } = dom (/) )
13		dm0	|- dom (/) = (/)
14	12 13	eqtrdi	|- ( -. A e. _V -> dom { A } = (/) )
15	14	unieqd	|- ( -. A e. _V -> U. dom { A } = U. (/) )
16		uni0	|- U. (/) = (/)
17	15 16	eqtrdi	|- ( -. A e. _V -> U. dom { A } = (/) )
18	9 17	eqtr4d	|- ( -. A e. _V -> ( 1st ` A ) = U. dom { A } )
19	8 18	pm2.61i	|- ( 1st ` A ) = U. dom { A }