Metamath Proof Explorer


Theorem ex-dm

Description: Example for df-dm . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-dm
|- ( F = { <. 2 , 6 >. , <. 3 , 9 >. } -> dom F = { 2 , 3 } )

Proof

Step Hyp Ref Expression
1 dmeq
 |-  ( F = { <. 2 , 6 >. , <. 3 , 9 >. } -> dom F = dom { <. 2 , 6 >. , <. 3 , 9 >. } )
2 6nn
 |-  6 e. NN
3 2 elexi
 |-  6 e. _V
4 9nn
 |-  9 e. NN
5 4 elexi
 |-  9 e. _V
6 3 5 dmprop
 |-  dom { <. 2 , 6 >. , <. 3 , 9 >. } = { 2 , 3 }
7 1 6 eqtrdi
 |-  ( F = { <. 2 , 6 >. , <. 3 , 9 >. } -> dom F = { 2 , 3 } )