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 ⊢ ∀ y Ⅎ x φ → a x b y φ ↔ b y φ

Proof

Step Hyp Ref Expression
1 nfa1 ⊢ Ⅎ y ∀ y Ⅎ x φ
2 sb6 ⊢ b y φ ↔ ∀ y y = b → φ
3 2 a1i ⊢ ∀ y Ⅎ x φ → b y φ ↔ ∀ y y = b → φ
4 2 biimpri ⊢ ∀ y y = b → φ → b y φ
5 4 axc4i ⊢ ∀ y y = b → φ → ∀ y b y φ
6 3 5 biimtrdi ⊢ ∀ y Ⅎ x φ → b y φ → ∀ y b y φ
7 1 6 nf5d ⊢ ∀ y Ⅎ x φ → Ⅎ y b y φ
8 1 7 nfim1 ⊢ Ⅎ y ∀ y Ⅎ x φ → b y φ
9 sbequ12 ⊢ y = b → φ ↔ b y φ
10 9 imbi2d ⊢ y = b → ∀ y Ⅎ x φ → φ ↔ ∀ y Ⅎ x φ → b y φ
11 8 10 equsalv ⊢ ∀ y y = b → ∀ y Ⅎ x φ → φ ↔ ∀ y Ⅎ x φ → b y φ
12 11 bicomi ⊢ ∀ y Ⅎ x φ → b y φ ↔ ∀ y y = b → ∀ y Ⅎ x φ → φ
13 nfv ⊢ Ⅎ x y = b
14 nfnf1 ⊢ Ⅎ x Ⅎ x φ
15 14 nfal ⊢ Ⅎ x ∀ y Ⅎ x φ
16 sp ⊢ ∀ y Ⅎ x φ → Ⅎ x φ
17 15 16 nfim1 ⊢ Ⅎ x ∀ y Ⅎ x φ → φ
18 13 17 nfim ⊢ Ⅎ x y = b → ∀ y Ⅎ x φ → φ
19 18 nfal ⊢ Ⅎ x ∀ y y = b → ∀ y Ⅎ x φ → φ
20 12 19 nfxfr ⊢ Ⅎ x ∀ y Ⅎ x φ → b y φ
21 pm5.5 ⊢ ∀ y Ⅎ x φ → ∀ y Ⅎ x φ → b y φ ↔ b y φ
22 15 21 nfbidf ⊢ ∀ y Ⅎ x φ → Ⅎ x ∀ y Ⅎ x φ → b y φ ↔ Ⅎ x b y φ
23 20 22 mpbii ⊢ ∀ y Ⅎ x φ → Ⅎ x b y φ
24 sbft ⊢ Ⅎ x b y φ → a x b y φ ↔ b y φ
25 23 24 syl ⊢ ∀ y Ⅎ x φ → a x b y φ ↔ b y φ