ex-ima

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

		Ref	Expression
	Assertion	ex-ima	$⊢ (F = \{⟨2, 6⟩, ⟨3, 9⟩\} \land B = \{1, 2\}) \to F [B] = \{6\}$

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [B] = ran ({F ↾}_{B})$
2		ex-res	$⊢ (F = \{⟨2, 6⟩, ⟨3, 9⟩\} \land B = \{1, 2\}) \to {F ↾}_{B} = \{⟨2, 6⟩\}$
3	2	rneqd	$⊢ (F = \{⟨2, 6⟩, ⟨3, 9⟩\} \land B = \{1, 2\}) \to ran ({F ↾}_{B}) = ran \{⟨2, 6⟩\}$
4	1 3	eqtrid	$⊢ (F = \{⟨2, 6⟩, ⟨3, 9⟩\} \land B = \{1, 2\}) \to F [B] = ran \{⟨2, 6⟩\}$
5		2ex	$⊢ 2 \in V$
6	5	rnsnop	$⊢ ran \{⟨2, 6⟩\} = \{6\}$
7	4 6	eqtrdi	$⊢ (F = \{⟨2, 6⟩, ⟨3, 9⟩\} \land B = \{1, 2\}) \to F [B] = \{6\}$

Metamath Proof Explorer