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

Proof

Step	Hyp	Ref	Expression
1		nfnf1	|- F/ x F/ x ph
2	1	nfal	|- F/ x A. y F/ x ph
3		nfich1	|- F/ x [ x <> y ] ph
4	2 3	nfan	|- F/ x ( A. y F/ x ph /\ [ x <> y ] ph )
5		dfich2	|- ( [ x <> y ] ph <-> A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) )
6		ichnfimlem	|- ( A. y F/ x ph -> ( [ a / x ] [ b / y ] ph <-> [ b / y ] ph ) )
7		ichnfimlem	|- ( A. y F/ x ph -> ( [ b / x ] [ a / y ] ph <-> [ a / y ] ph ) )
8	6 7	bibi12d	|- ( A. y F/ x ph -> ( ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) <-> ( [ b / y ] ph <-> [ a / y ] ph ) ) )
9		bicom1	|- ( ( [ b / y ] ph <-> [ a / y ] ph ) -> ( [ a / y ] ph <-> [ b / y ] ph ) )
10	8 9	biimtrdi	|- ( A. y F/ x ph -> ( ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) -> ( [ a / y ] ph <-> [ b / y ] ph ) ) )
11	10	2alimdv	|- ( A. y F/ x ph -> ( A. a A. b ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) -> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) ) )
12	5 11	biimtrid	|- ( A. y F/ x ph -> ( [ x <> y ] ph -> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) ) )
13	12	imp	|- ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) )
14		sbnf2	|- ( F/ y ph <-> A. a A. b ( [ a / y ] ph <-> [ b / y ] ph ) )
15	13 14	sylibr	|- ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> F/ y ph )
16	4 15	alrimi	|- ( ( A. y F/ x ph /\ [ x <> y ] ph ) -> A. x F/ y ph )