# Metamath Proof Explorer

## Theorem rexxpf

Description: Version of rexxp with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008) (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 rexxpf ${⊢}\exists {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {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 1 nfn ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
6 2 nfn ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬{\phi }$
7 3 nfn ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
8 4 notbid ${⊢}{x}=⟨{y},{z}⟩\to \left(¬{\phi }↔¬{\psi }\right)$
9 5 6 7 8 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 }$
10 ralnex ${⊢}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }↔¬\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
11 10 ralbii ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
12 9 11 bitri ${⊢}\forall {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
13 12 notbii ${⊢}¬\forall {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
14 dfrex2 ${⊢}\exists {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}¬{\phi }$
15 dfrex2 ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
16 13 14 15 3bitr4i ${⊢}\exists {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$