Theorem fvimage

Description: Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	fvimage	$$⊢\left(A\in V\wedge R\left[A\right]\in W\right)\to \mathrm{𝖨𝗆𝖺𝗀𝖾}R\left(A\right)=R\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		imaeq2	$$⊢x=A\to R\left[x\right]=R\left[A\right]$$
3		imageval	$$⊢\mathrm{𝖨𝗆𝖺𝗀𝖾}R=\left(x\in \mathrm{V}⟼R\left[x\right]\right)$$
4	2 3	fvmptg	$$⊢\left(A\in \mathrm{V}\wedge R\left[A\right]\in W\right)\to \mathrm{𝖨𝗆𝖺𝗀𝖾}R\left(A\right)=R\left[A\right]$$
5	1 4	sylan	$$⊢\left(A\in V\wedge R\left[A\right]\in W\right)\to \mathrm{𝖨𝗆𝖺𝗀𝖾}R\left(A\right)=R\left[A\right]$$