# Metamath Proof Explorer

## Theorem bj-nnfext

Description: See nfex and bj-nfext . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnfext ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 df-bj-nnf ${⊢}Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
2 1 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
3 simpl ${⊢}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)$
4 3 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)$
5 bj-nnflemee ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
6 4 5 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 2 6 sylbi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 simpr ${⊢}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 8 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
10 bj-nnflemae ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
11 9 10 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)\wedge \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
12 2 11 sylbi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
13 df-bj-nnf ${⊢}Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
14 7 12 13 sylanbrc ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ\text{'}{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$