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

Metamath Proof Explorer

Theorem fvmpts

Description: Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	fvmpts.1	$⊢ F = (x \in C ⟼ B)$
	Assertion	fvmpts	$⊢ (A \in C \land ⦋ A / x ⦌ B \in V) \to F (A) = ⦋ A / x ⦌ B$

Proof

Step	Hyp	Ref	Expression
1		fvmpts.1	$⊢ F = (x \in C ⟼ B)$
2		csbeq1	$⊢ y = A \to ⦋ y / x ⦌ B = ⦋ A / x ⦌ B$
3		nfcv	$⊢ \underline{Ⅎ} y B$
4		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
5		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
6	3 4 5	cbvmpt	$⊢ (x \in C ⟼ B) = (y \in C ⟼ ⦋ y / x ⦌ B)$
7	1 6	eqtri	$⊢ F = (y \in C ⟼ ⦋ y / x ⦌ B)$
8	2 7	fvmptg	$⊢ (A \in C \land ⦋ A / x ⦌ B \in V) \to F (A) = ⦋ A / x ⦌ B$