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 ⊢ ∀ y Ⅎ x φ ∧ x ⇄ y φ → ∀ x Ⅎ y φ

Proof

Step Hyp Ref Expression
1 nfnf1 ⊢ Ⅎ x Ⅎ x φ
2 1 nfal ⊢ Ⅎ x ∀ y Ⅎ x φ
3 nfich1 ⊢ Ⅎ x x ⇄ y φ
4 2 3 nfan ⊢ Ⅎ x ∀ y Ⅎ x φ ∧ x ⇄ y φ
5 dfich2 ⊢ x ⇄ y φ ↔ ∀ a ∀ b a x b y φ ↔ b x a y φ
6 ichnfimlem ⊢ ∀ y Ⅎ x φ → a x b y φ ↔ b y φ
7 ichnfimlem ⊢ ∀ y Ⅎ x φ → b x a y φ ↔ a y φ
8 6 7 bibi12d ⊢ ∀ y Ⅎ x φ → a x b y φ ↔ b x a y φ ↔ b y φ ↔ a y φ
9 bicom1 ⊢ b y φ ↔ a y φ → a y φ ↔ b y φ
10 8 9 biimtrdi ⊢ ∀ y Ⅎ x φ → a x b y φ ↔ b x a y φ → a y φ ↔ b y φ
11 10 2alimdv ⊢ ∀ y Ⅎ x φ → ∀ a ∀ b a x b y φ ↔ b x a y φ → ∀ a ∀ b a y φ ↔ b y φ
12 5 11 biimtrid ⊢ ∀ y Ⅎ x φ → x ⇄ y φ → ∀ a ∀ b a y φ ↔ b y φ
13 12 imp ⊢ ∀ y Ⅎ x φ ∧ x ⇄ y φ → ∀ a ∀ b a y φ ↔ b y φ
14 sbnf2 ⊢ Ⅎ y φ ↔ ∀ a ∀ b a y φ ↔ b y φ
15 13 14 sylibr ⊢ ∀ y Ⅎ x φ ∧ x ⇄ y φ → Ⅎ y φ
16 4 15 alrimi ⊢ ∀ y Ⅎ x φ ∧ x ⇄ y φ → ∀ x Ⅎ y φ