Theorem aovmpt4g

Description: Value of a function given by the maps-to notation, analogous to ovmpt4g . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	aovmpt4g.3	|- F = ( x e. A , y e. B |-> C )
Assertion	aovmpt4g	|- ( ( x e. A /\ y e. B /\ C e. V ) -> (( x F y )) = C )

Proof

Step	Hyp	Ref	Expression
1		aovmpt4g.3	|- F = ( x e. A , y e. B |-> C )
2	1	dmmpog	|- ( C e. V -> dom F = ( A X. B ) )
3		opelxpi	|- ( ( x e. A /\ y e. B ) -> <. x , y >. e. ( A X. B ) )
4		eleq2	|- ( dom F = ( A X. B ) -> ( <. x , y >. e. dom F <-> <. x , y >. e. ( A X. B ) ) )
5	3 4	imbitrrid	|- ( dom F = ( A X. B ) -> ( ( x e. A /\ y e. B ) -> <. x , y >. e. dom F ) )
6	2 5	syl	|- ( C e. V -> ( ( x e. A /\ y e. B ) -> <. x , y >. e. dom F ) )
7	6	impcom	|- ( ( ( x e. A /\ y e. B ) /\ C e. V ) -> <. x , y >. e. dom F )
8	7	3impa	|- ( ( x e. A /\ y e. B /\ C e. V ) -> <. x , y >. e. dom F )
9	1	mpofun	|- Fun F
10		funres	|- ( Fun F -> Fun ( F |` { <. x , y >. } ) )
11	9 10	ax-mp	|- Fun ( F |` { <. x , y >. } )
12		df-dfat	|- ( F defAt <. x , y >. <-> ( <. x , y >. e. dom F /\ Fun ( F |` { <. x , y >. } ) ) )
13		aovfundmoveq	|- ( F defAt <. x , y >. -> (( x F y )) = ( x F y ) )
14	12 13	sylbir	|- ( ( <. x , y >. e. dom F /\ Fun ( F |` { <. x , y >. } ) ) -> (( x F y )) = ( x F y ) )
15	8 11 14	sylancl	|- ( ( x e. A /\ y e. B /\ C e. V ) -> (( x F y )) = ( x F y ) )
16	1	ovmpt4g	|- ( ( x e. A /\ y e. B /\ C e. V ) -> ( x F y ) = C )
17	15 16	eqtrd	|- ( ( x e. A /\ y e. B /\ C e. V ) -> (( x F y )) = C )