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

Metamath Proof Explorer

Theorem fvmpt2

Description: Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010)

		Ref	Expression
	Hypothesis	mptrcl.1	$⊢ F = (x \in A ⟼ B)$
	Assertion	fvmpt2	$⊢ (x \in A \land B \in C) \to F (x) = B$

Step	Hyp	Ref	Expression
1		mptrcl.1	$⊢ F = (x \in A ⟼ B)$
2	1	fvmpt2i	$⊢ x \in A \to F (x) = I (B)$
3		fvi	$⊢ B \in C \to I (B) = B$
4	2 3	sylan9eq	$⊢ (x \in A \land B \in C) \to F (x) = B$