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

Metamath Proof Explorer

Theorem fvmpt3i

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvmpt3.a	$⊢ x = A \to B = C$
	fvmpt3.b	$⊢ F = (x \in D ⟼ B)$
	fvmpt3i.c	$⊢ B \in V$
Assertion	fvmpt3i	$⊢ A \in D \to F (A) = C$

Proof

Step	Hyp	Ref	Expression
1		fvmpt3.a	$⊢ x = A \to B = C$
2		fvmpt3.b	$⊢ F = (x \in D ⟼ B)$
3		fvmpt3i.c	$⊢ B \in V$
4	3	a1i	$⊢ x \in D \to B \in V$
5	1 2 4	fvmpt3	$⊢ A \in D \to F (A) = C$