Theorem ovmpordxf

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$$
	ovmpordxf.px	$$⊢Ⅎx\phi$$
	ovmpordxf.py	$$⊢Ⅎy\phi$$
	ovmpordxf.ay	$$⊢\underset{\_}{Ⅎ}yA$$
	ovmpordxf.bx	$$⊢\underset{\_}{Ⅎ}xB$$
	ovmpordxf.sx	$$⊢\underset{\_}{Ⅎ}xS$$
	ovmpordxf.sy	$$⊢\underset{\_}{Ⅎ}yS$$
Assertion	ovmpordxf	$$⊢\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		ovmpordxf.px	$$⊢Ⅎx\phi$$
8		ovmpordxf.py	$$⊢Ⅎy\phi$$
9		ovmpordxf.ay	$$⊢\underset{\_}{Ⅎ}yA$$
10		ovmpordxf.bx	$$⊢\underset{\_}{Ⅎ}xB$$
11		ovmpordxf.sx	$$⊢\underset{\_}{Ⅎ}xS$$
12		ovmpordxf.sy	$$⊢\underset{\_}{Ⅎ}yS$$
13	1	oveqd	$$⊢\phi \to AFB=A\left(x\in C,y\in D⟼R\right)B$$
14		eqid	$$⊢\left(x\in C,y\in D⟼R\right)=\left(x\in C,y\in D⟼R\right)$$
15	14	ovmpt4g	$$⊢\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R$$
16	15	a1i	$$⊢\phi \to \left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)$$
17	8 16	alrimi	$$⊢\phi \to \forall y\left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)$$
18	5 17	spsbcd	$$⊢\phi \to \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)$$
19	7 18	alrimi	$$⊢\phi \to \forall x\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)$$
20	4 19	spsbcd	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)$$
21	5	adantr	$$⊢\left(\phi \wedge x=A\right)\to B\in D$$
22	4	ad2antrr	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to A\in L$$
23		simpr	$$⊢\left(\phi \wedge x=A\right)\to x=A$$
24	23	adantr	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to x=A$$
25	3	adantlr	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to C=L$$
26	22 24 25	3eltr4d	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to x\in C$$
27	5	ad2antrr	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to B\in D$$
28		eleq1	$$⊢y=B\to \left(y\in D\leftrightarrow B\in D\right)$$
29	28	adantl	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to \left(y\in D\leftrightarrow B\in D\right)$$
30	27 29	mpbird	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to y\in D$$
31	2	anassrs	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to R=S$$
32	6	ad2antrr	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to S\in X$$
33	31 32	eqeltrd	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to R\in X$$
34		biimt	$$⊢\left(x\in C\wedge y\in D\wedge R\in X\right)\to \left(x\left(x\in C,y\in D⟼R\right)y=R\leftrightarrow \left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)\right)$$
35	26 30 33 34	syl3anc	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to \left(x\left(x\in C,y\in D⟼R\right)y=R\leftrightarrow \left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)\right)$$
36		simpr	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to y=B$$
37	24 36	oveq12d	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to x\left(x\in C,y\in D⟼R\right)y=A\left(x\in C,y\in D⟼R\right)B$$
38	37 31	eqeq12d	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to \left(x\left(x\in C,y\in D⟼R\right)y=R\leftrightarrow A\left(x\in C,y\in D⟼R\right)B=S\right)$$
39	35 38	bitr3d	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to \left(\left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)\leftrightarrow A\left(x\in C,y\in D⟼R\right)B=S\right)$$
40	9	nfeq2	$$⊢Ⅎyx=A$$
41	8 40	nfan	$$⊢Ⅎy\left(\phi \wedge x=A\right)$$
42		nfmpo2	$$⊢\underset{\_}{Ⅎ}y\left(x\in C,y\in D⟼R\right)$$
43		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
44	9 42 43	nfov	$$⊢\underset{\_}{Ⅎ}y\left(A\left(x\in C,y\in D⟼R\right)B\right)$$
45	44 12	nfeq	$$⊢ℲyA\left(x\in C,y\in D⟼R\right)B=S$$
46	45	a1i	$$⊢\left(\phi \wedge x=A\right)\to ℲyA\left(x\in C,y\in D⟼R\right)B=S$$
47	21 39 41 46	sbciedf	$$⊢\left(\phi \wedge x=A\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)\leftrightarrow A\left(x\in C,y\in D⟼R\right)B=S\right)$$
48		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
49		nfmpo1	$$⊢\underset{\_}{Ⅎ}x\left(x\in C,y\in D⟼R\right)$$
50	48 49 10	nfov	$$⊢\underset{\_}{Ⅎ}x\left(A\left(x\in C,y\in D⟼R\right)B\right)$$
51	50 11	nfeq	$$⊢ℲxA\left(x\in C,y\in D⟼R\right)B=S$$
52	51	a1i	$$⊢\phi \to ℲxA\left(x\in C,y\in D⟼R\right)B=S$$
53	4 47 7 52	sbciedf	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\left(\left(x\in C\wedge y\in D\wedge R\in X\right)\to x\left(x\in C,y\in D⟼R\right)y=R\right)\leftrightarrow A\left(x\in C,y\in D⟼R\right)B=S\right)$$
54	20 53	mpbid	$$⊢\phi \to A\left(x\in C,y\in D⟼R\right)B=S$$
55	13 54	eqtrd	$$⊢\phi \to AFB=S$$