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

Metamath Proof Explorer

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	$⊢ (A \in V \land R [A] \in W) \to 𝖨𝗆𝖺𝗀𝖾 R (A) = R [A]$

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