# Metamath Proof Explorer

## Theorem nfbidv

Description: An equality theorem for nonfreeness. See nfbidf for a version without disjoint variable condition but requiring more axioms. (Contributed by Mario Carneiro, 4-Oct-2016) Remove dependency on ax-6 , ax-7 , ax-12 by adapting proof of nfbidf . (Revised by BJ, 25-Sep-2022)

Ref Expression
Hypothesis albidv.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
Assertion nfbidv ${⊢}{\phi }\to \left(Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }↔Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 albidv.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
2 1 exbidv ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
3 1 albidv ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 2 3 imbi12d ${⊢}{\phi }\to \left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\right)$
5 df-nf ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 df-nf ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
7 4 5 6 3bitr4g ${⊢}{\phi }\to \left(Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }↔Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$