This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) → ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) ) )
11 10 2alimdv ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) ) )
12 5 11 biimtrid ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑥 ⇄ 𝑦 ] 𝜑 → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) ) )
13 12 imp ⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
14 sbnf2 ⊢ ( Ⅎ 𝑦 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
15 13 14 sylibr ⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → Ⅎ 𝑦 𝜑 )
16 4 15 alrimi ⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ [ 𝑥 ⇄ 𝑦 ] 𝜑 ) → ∀ 𝑥 Ⅎ 𝑦 𝜑 )