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	|- F/_ x A
Assertion	bj-mptval	|- ( A. x e. A B e. V -> ( X e. A -> ( ( ( x e. A |-> B ) ` X ) = Y <-> X ( x e. A |-> B ) Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-mptval.nf	|- F/_ x A
2	1	fnmptf	|- ( A. x e. A B e. V -> ( x e. A |-> B ) Fn A )
3		fnbrfvb	|- ( ( ( x e. A |-> B ) Fn A /\ X e. A ) -> ( ( ( x e. A |-> B ) ` X ) = Y <-> X ( x e. A |-> B ) Y ) )
4	3	ex	|- ( ( x e. A |-> B ) Fn A -> ( X e. A -> ( ( ( x e. A |-> B ) ` X ) = Y <-> X ( x e. A |-> B ) Y ) ) )
5	2 4	syl	|- ( A. x e. A B e. V -> ( X e. A -> ( ( ( x e. A |-> B ) ` X ) = Y <-> X ( x e. A |-> B ) Y ) ) )