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	⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → dom 𝐹 = { 2 , 3 } )

Proof

Step	Hyp	Ref	Expression
1		dmeq	⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → dom 𝐹 = dom { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } )
2		6nn	⊢ 6 ∈ ℕ
3	2	elexi	⊢ 6 ∈ V
4		9nn	⊢ 9 ∈ ℕ
5	4	elexi	⊢ 9 ∈ V
6	3 5	dmprop	⊢ dom { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = { 2 , 3 }
7	1 6	eqtrdi	⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → dom 𝐹 = { 2 , 3 } )