Metamath Proof Explorer


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 φ F = x C , y D R
ovmpordx.2 φ x = A y = B R = S
ovmpordx.3 φ y = B C = L
ovmpordx.4 φ A L
ovmpordx.5 φ B D
ovmpordx.6 φ S X
ovmpordxf.px x φ
ovmpordxf.py y φ
ovmpordxf.ay _ y A
ovmpordxf.bx _ x B
ovmpordxf.sx _ x S
ovmpordxf.sy _ y S
Assertion ovmpordxf φ A F B = S

Proof

Step Hyp Ref Expression
1 ovmpordx.1 φ F = x C , y D R
2 ovmpordx.2 φ x = A y = B R = S
3 ovmpordx.3 φ y = B C = L
4 ovmpordx.4 φ A L
5 ovmpordx.5 φ B D
6 ovmpordx.6 φ S X
7 ovmpordxf.px x φ
8 ovmpordxf.py y φ
9 ovmpordxf.ay _ y A
10 ovmpordxf.bx _ x B
11 ovmpordxf.sx _ x S
12 ovmpordxf.sy _ y S
13 1 oveqd φ A F B = A x C , y D R B
14 eqid x C , y D R = x C , y D R
15 14 ovmpt4g x C y D R X x x C , y D R y = R
16 15 a1i φ x C y D R X x x C , y D R y = R
17 8 16 alrimi φ y x C y D R X x x C , y D R y = R
18 5 17 spsbcd φ [˙B / y]˙ x C y D R X x x C , y D R y = R
19 7 18 alrimi φ x [˙B / y]˙ x C y D R X x x C , y D R y = R
20 4 19 spsbcd φ [˙A / x]˙ [˙B / y]˙ x C y D R X x x C , y D R y = R
21 5 adantr φ x = A B D
22 4 ad2antrr φ x = A y = B A L
23 simpr φ x = A x = A
24 23 adantr φ x = A y = B x = A
25 3 adantlr φ x = A y = B C = L
26 22 24 25 3eltr4d φ x = A y = B x C
27 5 ad2antrr φ x = A y = B B D
28 eleq1 y = B y D B D
29 28 adantl φ x = A y = B y D B D
30 27 29 mpbird φ x = A y = B y D
31 2 anassrs φ x = A y = B R = S
32 6 ad2antrr φ x = A y = B S X
33 31 32 eqeltrd φ x = A y = B R X
34 biimt x C y D R X x x C , y D R y = R x C y D R X x x C , y D R y = R
35 26 30 33 34 syl3anc φ x = A y = B x x C , y D R y = R x C y D R X x x C , y D R y = R
36 simpr φ x = A y = B y = B
37 24 36 oveq12d φ x = A y = B x x C , y D R y = A x C , y D R B
38 37 31 eqeq12d φ x = A y = B x x C , y D R y = R A x C , y D R B = S
39 35 38 bitr3d φ x = A y = B x C y D R X x x C , y D R y = R A x C , y D R B = S
40 9 nfeq2 y x = A
41 8 40 nfan y φ x = A
42 nfmpo2 _ y x C , y D R
43 nfcv _ y B
44 9 42 43 nfov _ y A x C , y D R B
45 44 12 nfeq y A x C , y D R B = S
46 45 a1i φ x = A y A x C , y D R B = S
47 21 39 41 46 sbciedf φ x = A [˙B / y]˙ x C y D R X x x C , y D R y = R A x C , y D R B = S
48 nfcv _ x A
49 nfmpo1 _ x x C , y D R
50 48 49 10 nfov _ x A x C , y D R B
51 50 11 nfeq x A x C , y D R B = S
52 51 a1i φ x A x C , y D R B = S
53 4 47 7 52 sbciedf φ [˙A / x]˙ [˙B / y]˙ x C y D R X x x C , y D R y = R A x C , y D R B = S
54 20 53 mpbid φ A x C , y D R B = S
55 13 54 eqtrd φ A F B = S