Theorem ovmpordx

Description: Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf . (Contributed by AV, 30-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		ovmpordx.1	$$⊢\phi \to F=\left(x\in C,y\in D⟼R\right)$$
2		ovmpordx.2	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R=S$$
3		ovmpordx.3	$$⊢\left(\phi \wedge y=B\right)\to C=L$$
4		ovmpordx.4	$$⊢\phi \to A\in L$$
5		ovmpordx.5	$$⊢\phi \to B\in D$$
6		ovmpordx.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	ovmpordxf	$$⊢\phi \to AFB=S$$