Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ichnfimlem Structured version   Visualization version   GIF version

Theorem ichnfimlem 43967
Description: Lemma for ichnfim 43968: A substitution of a non-free variable has no effect. (Contributed by Wolf Lammen, 6-Aug-2023.) Avoid ax-13 2382. (Revised by Gino Giotto, 1-May-2024.)
Assertion
Ref Expression
ichnfimlem (∀𝑦𝑥𝜑 → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
Distinct variable group:   𝑥,𝑏,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem ichnfimlem
StepHypRef Expression
1 nfa1 2153 . . . . . . 7 𝑦𝑦𝑥𝜑
2 sb6 2091 . . . . . . . . . 10 ([𝑏 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑏𝜑))
32a1i 11 . . . . . . . . 9 (∀𝑦𝑥𝜑 → ([𝑏 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑏𝜑)))
42biimpri 231 . . . . . . . . . 10 (∀𝑦(𝑦 = 𝑏𝜑) → [𝑏 / 𝑦]𝜑)
54axc4i 2333 . . . . . . . . 9 (∀𝑦(𝑦 = 𝑏𝜑) → ∀𝑦[𝑏 / 𝑦]𝜑)
63, 5syl6bi 256 . . . . . . . 8 (∀𝑦𝑥𝜑 → ([𝑏 / 𝑦]𝜑 → ∀𝑦[𝑏 / 𝑦]𝜑))
71, 6nf5d 2290 . . . . . . 7 (∀𝑦𝑥𝜑 → Ⅎ𝑦[𝑏 / 𝑦]𝜑)
81, 7nfim1 2198 . . . . . 6 𝑦(∀𝑦𝑥𝜑 → [𝑏 / 𝑦]𝜑)
9 sbequ12 2252 . . . . . . 7 (𝑦 = 𝑏 → (𝜑 ↔ [𝑏 / 𝑦]𝜑))
109imbi2d 344 . . . . . 6 (𝑦 = 𝑏 → ((∀𝑦𝑥𝜑𝜑) ↔ (∀𝑦𝑥𝜑 → [𝑏 / 𝑦]𝜑)))
118, 10equsalv 2267 . . . . 5 (∀𝑦(𝑦 = 𝑏 → (∀𝑦𝑥𝜑𝜑)) ↔ (∀𝑦𝑥𝜑 → [𝑏 / 𝑦]𝜑))
1211bicomi 227 . . . 4 ((∀𝑦𝑥𝜑 → [𝑏 / 𝑦]𝜑) ↔ ∀𝑦(𝑦 = 𝑏 → (∀𝑦𝑥𝜑𝜑)))
13 nfv 1915 . . . . . 6 𝑥 𝑦 = 𝑏
14 nfnf1 2156 . . . . . . . 8 𝑥𝑥𝜑
1514nfal 2334 . . . . . . 7 𝑥𝑦𝑥𝜑
16 sp 2181 . . . . . . 7 (∀𝑦𝑥𝜑 → Ⅎ𝑥𝜑)
1715, 16nfim1 2198 . . . . . 6 𝑥(∀𝑦𝑥𝜑𝜑)
1813, 17nfim 1897 . . . . 5 𝑥(𝑦 = 𝑏 → (∀𝑦𝑥𝜑𝜑))
1918nfal 2334 . . . 4 𝑥𝑦(𝑦 = 𝑏 → (∀𝑦𝑥𝜑𝜑))
2012, 19nfxfr 1854 . . 3 𝑥(∀𝑦𝑥𝜑 → [𝑏 / 𝑦]𝜑)
21 pm5.5 365 . . . 4 (∀𝑦𝑥𝜑 → ((∀𝑦𝑥𝜑 → [𝑏 / 𝑦]𝜑) ↔ [𝑏 / 𝑦]𝜑))
2215, 21nfbidf 2225 . . 3 (∀𝑦𝑥𝜑 → (Ⅎ𝑥(∀𝑦𝑥𝜑 → [𝑏 / 𝑦]𝜑) ↔ Ⅎ𝑥[𝑏 / 𝑦]𝜑))
2320, 22mpbii 236 . 2 (∀𝑦𝑥𝜑 → Ⅎ𝑥[𝑏 / 𝑦]𝜑)
24 sbft 2269 . 2 (Ⅎ𝑥[𝑏 / 𝑦]𝜑 → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
2523, 24syl 17 1 (∀𝑦𝑥𝜑 → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1536  wnf 1785  [wsb 2069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2143  ax-11 2159  ax-12 2176
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070
This theorem is referenced by:  ichnfim  43968
  Copyright terms: Public domain W3C validator