# Metamath Proof Explorer

## Theorem r19.12

Description: Restricted quantifier version of 19.12 . (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 30-May-2011) Avoid ax-13 , ax-ext . (Revised by Wolf Lammen, 17-Jun-2023)

Ref Expression
Assertion r19.12 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
3 nfra1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
4 2 3 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 4 nfex ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
6 1 5 nfxfr ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
7 ax-1 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 rsp ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({y}\in {B}\to {\phi }\right)$
9 8 com12 ${⊢}{y}\in {B}\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)$
10 9 reximdv ${⊢}{y}\in {B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
11 7 10 sylcom ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
12 6 11 ralrimi ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$