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 } )