# Metamath Proof Explorer

## Theorem ovmpodv2

Description: Alternate deduction version of ovmpo , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

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

### Proof

Step Hyp Ref Expression
1 ovmpodv2.1 ${⊢}{\phi }\to {A}\in {C}$
2 ovmpodv2.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to {B}\in {D}$
3 ovmpodv2.3 ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {R}\in {V}$
4 ovmpodv2.4 ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to {R}={S}$
5 eqidd ${⊢}{\phi }\to \left({x}\in {C},{y}\in {D}⟼{R}\right)=\left({x}\in {C},{y}\in {D}⟼{R}\right)$
6 4 eqeq2d ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to \left({A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={R}↔{A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={S}\right)$
7 6 biimpd ${⊢}\left({\phi }\wedge \left({x}={A}\wedge {y}={B}\right)\right)\to \left({A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={R}\to {A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={S}\right)$
8 nfmpo1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {C},{y}\in {D}⟼{R}\right)$
9 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
11 9 8 10 nfov ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}\right)$
12 11 nfeq1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={S}$
13 nfmpo2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {C},{y}\in {D}⟼{R}\right)$
14 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
15 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
16 14 13 15 nfov ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}\right)$
17 16 nfeq1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={S}$
18 1 2 3 7 8 12 13 17 ovmpodf ${⊢}{\phi }\to \left(\left({x}\in {C},{y}\in {D}⟼{R}\right)=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={S}\right)$
19 5 18 mpd ${⊢}{\phi }\to {A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={S}$
20 oveq ${⊢}{F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {A}{F}{B}={A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}$
21 20 eqeq1d ${⊢}{F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to \left({A}{F}{B}={S}↔{A}\left({x}\in {C},{y}\in {D}⟼{R}\right){B}={S}\right)$
22 19 21 syl5ibrcom ${⊢}{\phi }\to \left({F}=\left({x}\in {C},{y}\in {D}⟼{R}\right)\to {A}{F}{B}={S}\right)$