# Metamath Proof Explorer

## Theorem ralxpf

Description: Version of ralxp with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses ralxpf.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
ralxpf.2 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
ralxpf.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
ralxpf.4 ${⊢}{x}=⟨{y},{z}⟩\to \left({\phi }↔{\psi }\right)$
Assertion ralxpf ${⊢}\forall {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 ralxpf.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 ralxpf.2 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
3 ralxpf.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
4 ralxpf.4 ${⊢}{x}=⟨{y},{z}⟩\to \left({\phi }↔{\psi }\right)$
5 cbvralsvw ${⊢}\forall {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }$
6 cbvralsvw ${⊢}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\psi }↔\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }$
7 6 ralbii ${⊢}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\psi }↔\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }$
8 nfv ${⊢}Ⅎ{u}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
9 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
10 nfs1v ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\psi }$
11 9 10 nfralw ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\psi }$
12 sbequ12 ${⊢}{y}={u}\to \left({\psi }↔\left[{u}/{y}\right]{\psi }\right)$
13 12 ralbidv ${⊢}{y}={u}\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\psi }\right)$
14 8 11 13 cbvralw ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\psi }$
15 vex ${⊢}{u}\in \mathrm{V}$
16 vex ${⊢}{v}\in \mathrm{V}$
17 15 16 eqvinop ${⊢}{w}=⟨{u},{v}⟩↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{y},{z}⟩\wedge ⟨{y},{z}⟩=⟨{u},{v}⟩\right)$
18 1 nfsbv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }$
19 10 nfsbv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }$
20 18 19 nfbi ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
21 2 nfsbv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }$
22 nfs1v ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }$
23 21 22 nfbi ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
24 3 4 sbhypf ${⊢}{w}=⟨{y},{z}⟩\to \left(\left[{w}/{x}\right]{\phi }↔{\psi }\right)$
25 vex ${⊢}{y}\in \mathrm{V}$
26 vex ${⊢}{z}\in \mathrm{V}$
27 25 26 opth ${⊢}⟨{y},{z}⟩=⟨{u},{v}⟩↔\left({y}={u}\wedge {z}={v}\right)$
28 sbequ12 ${⊢}{z}={v}\to \left(\left[{u}/{y}\right]{\psi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
29 12 28 sylan9bb ${⊢}\left({y}={u}\wedge {z}={v}\right)\to \left({\psi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
30 27 29 sylbi ${⊢}⟨{y},{z}⟩=⟨{u},{v}⟩\to \left({\psi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
31 24 30 sylan9bb ${⊢}\left({w}=⟨{y},{z}⟩\wedge ⟨{y},{z}⟩=⟨{u},{v}⟩\right)\to \left(\left[{w}/{x}\right]{\phi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
32 23 31 exlimi ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{y},{z}⟩\wedge ⟨{y},{z}⟩=⟨{u},{v}⟩\right)\to \left(\left[{w}/{x}\right]{\phi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
33 20 32 exlimi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{y},{z}⟩\wedge ⟨{y},{z}⟩=⟨{u},{v}⟩\right)\to \left(\left[{w}/{x}\right]{\phi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
34 17 33 sylbi ${⊢}{w}=⟨{u},{v}⟩\to \left(\left[{w}/{x}\right]{\phi }↔\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }\right)$
35 34 ralxp ${⊢}\forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }↔\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left[{v}/{z}\right]\left[{u}/{y}\right]{\psi }$
36 7 14 35 3bitr4ri ${⊢}\forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
37 5 36 bitri ${⊢}\forall {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$