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=\left(x\in C,y\in D⟼R\right)$$
	ovmpogad.s	$$⊢\left(x=A\wedge y=B\right)\to R=S$$
	ovmpogad.1	$$⊢\phi \to A\in C$$
	ovmpogad.2	$$⊢\phi \to B\in D$$
	ovmpogad.v	$$⊢\phi \to S\in V$$
Assertion	ovmpogad	$$⊢\phi \to AFB=S$$

Proof

Step	Hyp	Ref	Expression
1		ovmpogad.f	$$⊢F=\left(x\in C,y\in D⟼R\right)$$
2		ovmpogad.s	$$⊢\left(x=A\wedge y=B\right)\to R=S$$
3		ovmpogad.1	$$⊢\phi \to A\in C$$
4		ovmpogad.2	$$⊢\phi \to B\in D$$
5		ovmpogad.v	$$⊢\phi \to S\in V$$
6	1	a1i	$$⊢\phi \to F=\left(x\in C,y\in D⟼R\right)$$
7	2	adantl	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R=S$$
8	6 7 3 4 5	ovmpod	$$⊢\phi \to AFB=S$$