# Metamath Proof Explorer

## Theorem ichnfb

Description: If x and y are interchangeable in ph , they are both free or both not free in ph . (Contributed by Wolf Lammen, 6-Aug-2023) (Revised by AV, 23-Sep-2023)

Ref Expression
Assertion ichnfb ${⊢}\left[{x}⇄{y}\right]{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 ichcom ${⊢}\left[{x}⇄{y}\right]{\phi }↔\left[{y}⇄{x}\right]{\phi }$
2 ichnfim ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \left[{y}⇄{x}\right]{\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 1 2 sylan2b ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \left[{x}⇄{y}\right]{\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 3 expcom ${⊢}\left[{x}⇄{y}\right]{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 ichnfim ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \left[{x}⇄{y}\right]{\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 5 expcom ${⊢}\left[{x}⇄{y}\right]{\phi }\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 4 6 impbid ${⊢}\left[{x}⇄{y}\right]{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$