Theorem ovmpod

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

	Ref	Expression
Hypotheses	ovmpod.1	$$⊢\phi \to F=\left(x\in C,y\in D⟼R\right)$$
	ovmpod.2	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R=S$$
	ovmpod.3	$$⊢\phi \to A\in C$$
	ovmpod.4	$$⊢\phi \to B\in D$$
	ovmpod.5	$$⊢\phi \to S\in X$$
Assertion	ovmpod	$$⊢\phi \to AFB=S$$

Proof

Step	Hyp	Ref	Expression
1		ovmpod.1	$$⊢\phi \to F=\left(x\in C,y\in D⟼R\right)$$
2		ovmpod.2	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R=S$$
3		ovmpod.3	$$⊢\phi \to A\in C$$
4		ovmpod.4	$$⊢\phi \to B\in D$$
5		ovmpod.5	$$⊢\phi \to S\in X$$
6		eqidd	$$⊢\left(\phi \wedge x=A\right)\to D=D$$
7	1 2 6 3 4 5	ovmpodx	$$⊢\phi \to AFB=S$$