Theorem ovmpogad

Description: Value of an operation given by a maps-to rule. Deduction form of ovmpoga . (Contributed by SN, 14-Mar-2025)

	Ref	Expression
Hypotheses	ovmpogad.f	|- F = ( x e. C , y e. D |-> R )
	ovmpogad.s	|- ( ( x = A /\ y = B ) -> R = S )
	ovmpogad.1	|- ( ph -> A e. C )
	ovmpogad.2	|- ( ph -> B e. D )
	ovmpogad.v	|- ( ph -> S e. V )
Assertion	ovmpogad	|- ( ph -> ( A F B ) = S )

Proof

Step	Hyp	Ref	Expression
1		ovmpogad.f	|- F = ( x e. C , y e. D |-> R )
2		ovmpogad.s	|- ( ( x = A /\ y = B ) -> R = S )
3		ovmpogad.1	|- ( ph -> A e. C )
4		ovmpogad.2	|- ( ph -> B e. D )
5		ovmpogad.v	|- ( ph -> S e. V )
6	1	a1i	|- ( ph -> F = ( x e. C , y e. D |-> R ) )
7	2	adantl	|- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
8	6 7 3 4 5	ovmpod	|- ( ph -> ( A F B ) = S )