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\rightleftarrows y\right]\phi \to \left(\forall xℲy\phi \leftrightarrow \forall yℲx\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ichcom	$$⊢\left[x\rightleftarrows y\right]\phi \leftrightarrow \left[y\rightleftarrows x\right]\phi$$
2		ichnfim	$$⊢\left(\forall xℲy\phi \wedge \left[y\rightleftarrows x\right]\phi \right)\to \forall yℲx\phi$$
3	1 2	sylan2b	$$⊢\left(\forall xℲy\phi \wedge \left[x\rightleftarrows y\right]\phi \right)\to \forall yℲx\phi$$
4	3	expcom	$$⊢\left[x\rightleftarrows y\right]\phi \to \left(\forall xℲy\phi \to \forall yℲx\phi \right)$$
5		ichnfim	$$⊢\left(\forall yℲx\phi \wedge \left[x\rightleftarrows y\right]\phi \right)\to \forall xℲy\phi$$
6	5	expcom	$$⊢\left[x\rightleftarrows y\right]\phi \to \left(\forall yℲx\phi \to \forall xℲy\phi \right)$$
7	4 6	impbid	$$⊢\left[x\rightleftarrows y\right]\phi \to \left(\forall xℲy\phi \leftrightarrow \forall yℲx\phi \right)$$