Theorem ichnfim

Description: If in an interchangeability context x is not free in ph , the same holds for y . (Contributed by Wolf Lammen, 6-Aug-2023) (Revised by AV, 23-Sep-2023)

	Ref	Expression
Assertion	ichnfim	$$⊢\left(\forall yℲx\phi \wedge \left[x\rightleftarrows y\right]\phi \right)\to \forall xℲy\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfnf1	$$⊢ℲxℲx\phi$$
2	1	nfal	$$⊢Ⅎx\forall yℲx\phi$$
3		nfich1	$$⊢Ⅎx\left[x\rightleftarrows y\right]\phi$$
4	2 3	nfan	$$⊢Ⅎx\left(\forall yℲx\phi \wedge \left[x\rightleftarrows y\right]\phi \right)$$
5		dfich2	$$⊢\left[x\rightleftarrows y\right]\phi \leftrightarrow \forall a\forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)$$
6		ichnfimlem	$$⊢\forall yℲx\phi \to \left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$
7		ichnfimlem	$$⊢\forall yℲx\phi \to \left(\left[b/x\right]\left[a/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)$$
8	6 7	bibi12d	$$⊢\forall yℲx\phi \to \left(\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)\leftrightarrow \left(\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)\right)$$
9		bicom1	$$⊢\left(\left[b/y\right]\phi \leftrightarrow \left[a/y\right]\phi \right)\to \left(\left[a/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$
10	8 9	syl6bi	$$⊢\forall yℲx\phi \to \left(\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)\to \left(\left[a/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)\right)$$
11	10	2alimdv	$$⊢\forall yℲx\phi \to \left(\forall a\forall b\left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/x\right]\left[a/y\right]\phi \right)\to \forall a\forall b\left(\left[a/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)\right)$$
12	5 11	biimtrid	$$⊢\forall yℲx\phi \to \left(\left[x\rightleftarrows y\right]\phi \to \forall a\forall b\left(\left[a/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)\right)$$
13	12	imp	$$⊢\left(\forall yℲx\phi \wedge \left[x\rightleftarrows y\right]\phi \right)\to \forall a\forall b\left(\left[a/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$
14		sbnf2	$$⊢Ⅎy\phi \leftrightarrow \forall a\forall b\left(\left[a/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$
15	13 14	sylibr	$$⊢\left(\forall yℲx\phi \wedge \left[x\rightleftarrows y\right]\phi \right)\to Ⅎy\phi$$
16	4 15	alrimi	$$⊢\left(\forall yℲx\phi \wedge \left[x\rightleftarrows y\right]\phi \right)\to \forall xℲy\phi$$