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 ) )

Metamath Proof Explorer

Theorem ichnfimlem

Proof