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	|- ( A. y F/ x ph -> ( [ a / x ] [ b / y ] ph <-> [ b / y ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfa1	|- F/ y A. y F/ x ph
2		sb6	|- ( [ b / y ] ph <-> A. y ( y = b -> ph ) )
3	2	a1i	|- ( A. y F/ x ph -> ( [ b / y ] ph <-> A. y ( y = b -> ph ) ) )
4	2	biimpri	|- ( A. y ( y = b -> ph ) -> [ b / y ] ph )
5	4	axc4i	|- ( A. y ( y = b -> ph ) -> A. y [ b / y ] ph )
6	3 5	biimtrdi	|- ( A. y F/ x ph -> ( [ b / y ] ph -> A. y [ b / y ] ph ) )
7	1 6	nf5d	|- ( A. y F/ x ph -> F/ y [ b / y ] ph )
8	1 7	nfim1	|- F/ y ( A. y F/ x ph -> [ b / y ] ph )
9		sbequ12	|- ( y = b -> ( ph <-> [ b / y ] ph ) )
10	9	imbi2d	|- ( y = b -> ( ( A. y F/ x ph -> ph ) <-> ( A. y F/ x ph -> [ b / y ] ph ) ) )
11	8 10	equsalv	|- ( A. y ( y = b -> ( A. y F/ x ph -> ph ) ) <-> ( A. y F/ x ph -> [ b / y ] ph ) )
12	11	bicomi	|- ( ( A. y F/ x ph -> [ b / y ] ph ) <-> A. y ( y = b -> ( A. y F/ x ph -> ph ) ) )
13		nfv	|- F/ x y = b
14		nfnf1	|- F/ x F/ x ph
15	14	nfal	|- F/ x A. y F/ x ph
16		sp	|- ( A. y F/ x ph -> F/ x ph )
17	15 16	nfim1	|- F/ x ( A. y F/ x ph -> ph )
18	13 17	nfim	|- F/ x ( y = b -> ( A. y F/ x ph -> ph ) )
19	18	nfal	|- F/ x A. y ( y = b -> ( A. y F/ x ph -> ph ) )
20	12 19	nfxfr	|- F/ x ( A. y F/ x ph -> [ b / y ] ph )
21		pm5.5	|- ( A. y F/ x ph -> ( ( A. y F/ x ph -> [ b / y ] ph ) <-> [ b / y ] ph ) )
22	15 21	nfbidf	|- ( A. y F/ x ph -> ( F/ x ( A. y F/ x ph -> [ b / y ] ph ) <-> F/ x [ b / y ] ph ) )
23	20 22	mpbii	|- ( A. y F/ x ph -> F/ x [ b / y ] ph )
24		sbft	|- ( F/ x [ b / y ] ph -> ( [ a / x ] [ b / y ] ph <-> [ b / y ] ph ) )
25	23 24	syl	|- ( A. y F/ x ph -> ( [ a / x ] [ b / y ] ph <-> [ b / y ] ph ) )