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

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⟩\} \to dom F = \{2, 3\}$

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