Theorem ichnfimlem

Description: Lemma for ichnfim : A substitution for a nonfree variable has no effect. (Contributed by Wolf Lammen, 6-Aug-2023) Avoid ax-13 . (Revised by GG, 1-May-2024)

	Ref	Expression
Assertion	ichnfimlem	$$⊢\forall yℲx\phi \to \left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎy\forall yℲx\phi$$
2		sb6	$$⊢\left[b/y\right]\phi \leftrightarrow \forall y\left(y=b\to \phi \right)$$
3	2	a1i	$$⊢\forall yℲx\phi \to \left(\left[b/y\right]\phi \leftrightarrow \forall y\left(y=b\to \phi \right)\right)$$
4	2	biimpri	$$⊢\forall y\left(y=b\to \phi \right)\to \left[b/y\right]\phi$$
5	4	axc4i	$$⊢\forall y\left(y=b\to \phi \right)\to \forall y\left[b/y\right]\phi$$
6	3 5	biimtrdi	$$⊢\forall yℲx\phi \to \left(\left[b/y\right]\phi \to \forall y\left[b/y\right]\phi \right)$$
7	1 6	nf5d	$$⊢\forall yℲx\phi \to Ⅎy\left[b/y\right]\phi$$
8	1 7	nfim1	$$⊢Ⅎy\left(\forall yℲx\phi \to \left[b/y\right]\phi \right)$$
9		sbequ12	$$⊢y=b\to \left(\phi \leftrightarrow \left[b/y\right]\phi \right)$$
10	9	imbi2d	$$⊢y=b\to \left(\left(\forall yℲx\phi \to \phi \right)\leftrightarrow \left(\forall yℲx\phi \to \left[b/y\right]\phi \right)\right)$$
11	8 10	equsalv	$$⊢\forall y\left(y=b\to \left(\forall yℲx\phi \to \phi \right)\right)\leftrightarrow \left(\forall yℲx\phi \to \left[b/y\right]\phi \right)$$
12	11	bicomi	$$⊢\left(\forall yℲx\phi \to \left[b/y\right]\phi \right)\leftrightarrow \forall y\left(y=b\to \left(\forall yℲx\phi \to \phi \right)\right)$$
13		nfv	$$⊢Ⅎxy=b$$
14		nfnf1	$$⊢ℲxℲx\phi$$
15	14	nfal	$$⊢Ⅎx\forall yℲx\phi$$
16		sp	$$⊢\forall yℲx\phi \to Ⅎx\phi$$
17	15 16	nfim1	$$⊢Ⅎx\left(\forall yℲx\phi \to \phi \right)$$
18	13 17	nfim	$$⊢Ⅎx\left(y=b\to \left(\forall yℲx\phi \to \phi \right)\right)$$
19	18	nfal	$$⊢Ⅎx\forall y\left(y=b\to \left(\forall yℲx\phi \to \phi \right)\right)$$
20	12 19	nfxfr	$$⊢Ⅎx\left(\forall yℲx\phi \to \left[b/y\right]\phi \right)$$
21		pm5.5	$$⊢\forall yℲx\phi \to \left(\left(\forall yℲx\phi \to \left[b/y\right]\phi \right)\leftrightarrow \left[b/y\right]\phi \right)$$
22	15 21	nfbidf	$$⊢\forall yℲx\phi \to \left(Ⅎx\left(\forall yℲx\phi \to \left[b/y\right]\phi \right)\leftrightarrow Ⅎx\left[b/y\right]\phi \right)$$
23	20 22	mpbii	$$⊢\forall yℲx\phi \to Ⅎx\left[b/y\right]\phi$$
24		sbft	$$⊢Ⅎx\left[b/y\right]\phi \to \left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$
25	23 24	syl	$$⊢\forall yℲx\phi \to \left(\left[a/x\right]\left[b/y\right]\phi \leftrightarrow \left[b/y\right]\phi \right)$$