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=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to \mathrm{dom}F=\left\{2,3\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmeq	$$⊢F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to \mathrm{dom}F=\mathrm{dom}\left\{⟨2,6⟩,⟨3,9⟩\right\}$$
2		6nn	$$⊢6\in \mathbb{N}$$
3	2	elexi	$$⊢6\in \mathrm{V}$$
4		9nn	$$⊢9\in \mathbb{N}$$
5	4	elexi	$$⊢9\in \mathrm{V}$$
6	3 5	dmprop	$$⊢\mathrm{dom}\left\{⟨2,6⟩,⟨3,9⟩\right\}=\left\{2,3\right\}$$
7	1 6	eqtrdi	$$⊢F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to \mathrm{dom}F=\left\{2,3\right\}$$