Theorem ex-ima

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

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

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢F\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)$$
2		ex-res	$$⊢\left(F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge B=\left\{1,2\right\}\right)\to {F\upharpoonright }_B=\left\{⟨2,6⟩\right\}$$
3	2	rneqd	$$⊢\left(F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge B=\left\{1,2\right\}\right)\to \mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}\left\{⟨2,6⟩\right\}$$
4	1 3	syl5eq	$$⊢\left(F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge B=\left\{1,2\right\}\right)\to F\left[B\right]=\mathrm{ran}\left\{⟨2,6⟩\right\}$$
5		2ex	$$⊢2\in \mathrm{V}$$
6	5	rnsnop	$$⊢\mathrm{ran}\left\{⟨2,6⟩\right\}=\left\{6\right\}$$
7	4 6	eqtrdi	$$⊢\left(F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge B=\left\{1,2\right\}\right)\to F\left[B\right]=\left\{6\right\}$$