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	⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → ∀ 𝑥 Ⅎ 𝑦 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfnf1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝜑
2	1	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 Ⅎ 𝑥 𝜑
3		nfich1	⊢ Ⅎ 𝑥 [ 𝑥 ⇄ 𝑦 ] 𝜑
4	2 3	nfan	⊢ Ⅎ 𝑥 ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 )
5		dfich2	⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) )
6		ichnfimlem	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
7		ichnfimlem	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) )
8	6 7	bibi12d	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) ↔ ( [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) ) )
9		bicom1	⊢ ( ( [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑦 ] 𝜑 ) → ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
10	8 9	syl6bi	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) → ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) ) )
11	10	2alimdv	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) ) )
12	5 11	syl5bi	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑥 ⇄ 𝑦 ] 𝜑 → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) ) )
13	12	imp	⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
14		sbnf2	⊢ ( Ⅎ 𝑦 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
15	13 14	sylibr	⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → Ⅎ 𝑦 𝜑 )
16	4 15	alrimi	⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → ∀ 𝑥 Ⅎ 𝑦 𝜑 )