This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 }