Theorem bj-mptval

Description: Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020)

	Ref	Expression
Hypothesis	bj-mptval.nf	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	bj-mptval	$$⊢\forall x\in AB\in V\to \left(X\in A\to \left(\left(x\in A⟼B\right)\left(X\right)=Y\leftrightarrow X\left(x\in A⟼B\right)Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-mptval.nf	$$⊢\underset{\_}{Ⅎ}xA$$
2	1	fnmptf	$$⊢\forall x\in AB\in V\to \left(x\in A⟼B\right)FnA$$
3		fnbrfvb	$$⊢\left(\left(x\in A⟼B\right)FnA\wedge X\in A\right)\to \left(\left(x\in A⟼B\right)\left(X\right)=Y\leftrightarrow X\left(x\in A⟼B\right)Y\right)$$
4	3	ex	$$⊢\left(x\in A⟼B\right)FnA\to \left(X\in A\to \left(\left(x\in A⟼B\right)\left(X\right)=Y\leftrightarrow X\left(x\in A⟼B\right)Y\right)\right)$$
5	2 4	syl	$$⊢\forall x\in AB\in V\to \left(X\in A\to \left(\left(x\in A⟼B\right)\left(X\right)=Y\leftrightarrow X\left(x\in A⟼B\right)Y\right)\right)$$