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

Metamath Proof Explorer

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 ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 Ⅎ 𝑥 𝜑
2 sb6 ⊢ ( [ 𝑏 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑏 → 𝜑 ) )
3 2 a1i ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑏 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑏 → 𝜑 ) ) )
4 2 biimpri ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑏 → 𝜑 ) → [ 𝑏 / 𝑦 ] 𝜑 )
5 4 axc4i ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑏 → 𝜑 ) → ∀ 𝑦 [ 𝑏 / 𝑦 ] 𝜑 )
6 3 5 biimtrdi ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑏 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑏 / 𝑦 ] 𝜑 ) )
7 1 6 nf5d ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → Ⅎ 𝑦 [ 𝑏 / 𝑦 ] 𝜑 )
8 1 7 nfim1 ⊢ Ⅎ 𝑦 ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → [ 𝑏 / 𝑦 ] 𝜑 )
9 sbequ12 ⊢ ( 𝑦 = 𝑏 → ( 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
10 9 imbi2d ⊢ ( 𝑦 = 𝑏 → ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → 𝜑 ) ↔ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → [ 𝑏 / 𝑦 ] 𝜑 ) ) )
11 8 10 equsalv ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑏 → ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → 𝜑 ) ) ↔ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → [ 𝑏 / 𝑦 ] 𝜑 ) )
12 11 bicomi ⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → [ 𝑏 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑏 → ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → 𝜑 ) ) )
13 nfv ⊢ Ⅎ 𝑥 𝑦 = 𝑏
14 nfnf1 ⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝜑
15 14 nfal ⊢ Ⅎ 𝑥 ∀ 𝑦 Ⅎ 𝑥 𝜑
16 sp ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )
17 15 16 nfim1 ⊢ Ⅎ 𝑥 ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → 𝜑 )
18 13 17 nfim ⊢ Ⅎ 𝑥 ( 𝑦 = 𝑏 → ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → 𝜑 ) )
19 18 nfal ⊢ Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑏 → ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → 𝜑 ) )
20 12 19 nfxfr ⊢ Ⅎ 𝑥 ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → [ 𝑏 / 𝑦 ] 𝜑 )
21 pm5.5 ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → [ 𝑏 / 𝑦 ] 𝜑 ) ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
22 15 21 nfbidf ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( Ⅎ 𝑥 ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → [ 𝑏 / 𝑦 ] 𝜑 ) ↔ Ⅎ 𝑥 [ 𝑏 / 𝑦 ] 𝜑 ) )
23 20 22 mpbii ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 [ 𝑏 / 𝑦 ] 𝜑 )
24 sbft ⊢ ( Ⅎ 𝑥 [ 𝑏 / 𝑦 ] 𝜑 → ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
25 23 24 syl ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )