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 Gino Giotto, 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 syl6bi 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 φ