Theorem ovmpodx

Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	ovmpodx.1	|- ( ph -> F = ( x e. C , y e. D |-> R ) )
	ovmpodx.2	|- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
	ovmpodx.3	|- ( ( ph /\ x = A ) -> D = L )
	ovmpodx.4	|- ( ph -> A e. C )
	ovmpodx.5	|- ( ph -> B e. L )
	ovmpodx.6	|- ( ph -> S e. X )
Assertion	ovmpodx	|- ( ph -> ( A F B ) = S )

Proof

Step	Hyp	Ref	Expression
1		ovmpodx.1	|- ( ph -> F = ( x e. C , y e. D |-> R ) )
2		ovmpodx.2	|- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
3		ovmpodx.3	|- ( ( ph /\ x = A ) -> D = L )
4		ovmpodx.4	|- ( ph -> A e. C )
5		ovmpodx.5	|- ( ph -> B e. L )
6		ovmpodx.6	|- ( ph -> S e. X )
7		nfv	|- F/ x ph
8		nfv	|- F/ y ph
9		nfcv	|- F/_ y A
10		nfcv	|- F/_ x B
11		nfcv	|- F/_ x S
12		nfcv	|- F/_ y S
13	1 2 3 4 5 6 7 8 9 10 11 12	ovmpodxf	|- ( ph -> ( A F B ) = S )