fvmpt2f

Description: Value of a function given by the maps-to notation. (Contributed by Thierry Arnoux, 9-Mar-2017)

		Ref	Expression
	Hypothesis	fvmpt2f.0	$⊢ \underline{Ⅎ} x A$
	Assertion	fvmpt2f	$⊢ (x \in A \land B \in C) \to (x \in A ⟼ B) (x) = B$

Step	Hyp	Ref	Expression
1		fvmpt2f.0	$⊢ \underline{Ⅎ} x A$
2		csbeq1	$⊢ y = x \to ⦋ y / x ⦌ B = ⦋ x / x ⦌ B$
3		csbid	$⊢ ⦋ x / x ⦌ B = B$
4	2 3	eqtrdi	$⊢ y = x \to ⦋ y / x ⦌ B = B$
5		nfcv	$⊢ \underline{Ⅎ} y A$
6		nfcv	$⊢ \underline{Ⅎ} y B$
7		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
8		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
9	1 5 6 7 8	cbvmptf	$⊢ (x \in A ⟼ B) = (y \in A ⟼ ⦋ y / x ⦌ B)$
10	4 9	fvmptg	$⊢ (x \in A \land B \in C) \to (x \in A ⟼ B) (x) = B$

Metamath Proof Explorer