Metamath Proof Explorer


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 }