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	$$⊢\phi \to F=\left(x\in C,y\in D⟼R\right)$$
	ovmpodx.2	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R=S$$
	ovmpodx.3	$$⊢\left(\phi \wedge x=A\right)\to D=L$$
	ovmpodx.4	$$⊢\phi \to A\in C$$
	ovmpodx.5	$$⊢\phi \to B\in L$$
	ovmpodx.6	$$⊢\phi \to S\in X$$
Assertion	ovmpodx	$$⊢\phi \to AFB=S$$

Proof

Step	Hyp	Ref	Expression
1		ovmpodx.1	$$⊢\phi \to F=\left(x\in C,y\in D⟼R\right)$$
2		ovmpodx.2	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R=S$$
3		ovmpodx.3	$$⊢\left(\phi \wedge x=A\right)\to D=L$$
4		ovmpodx.4	$$⊢\phi \to A\in C$$
5		ovmpodx.5	$$⊢\phi \to B\in L$$
6		ovmpodx.6	$$⊢\phi \to S\in X$$
7		nfv	$$⊢Ⅎx\phi$$
8		nfv	$$⊢Ⅎy\phi$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}xS$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}yS$$
13	1 2 3 4 5 6 7 8 9 10 11 12	ovmpodxf	$$⊢\phi \to AFB=S$$