Metamath Proof Explorer

Theorem nfbidf

Description: An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)

Ref Expression
Hypotheses albid.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
albid.2 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
Assertion nfbidf ${⊢}{\phi }\to \left(Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }↔Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

Proof

Step Hyp Ref Expression
1 albid.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 albid.2 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
3 1 2 exbid ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 1 2 albid ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 3 4 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)$
6 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)$
7 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)$
8 5 6 7 3bitr4g ${⊢}{\phi }\to \left(Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }↔Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$