Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbal Structured version   Visualization version   GIF version

Theorem sbal 2163
 Description: Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 13-Aug-2023.)
Assertion
Ref Expression
sbal ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
Distinct variable groups:   𝑥,𝑦   𝑥,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem sbal
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 alcom 2160 . 2 (∀𝑤𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)) ↔ ∀𝑥𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
2 19.21v 1940 . . . . . . 7 (∀𝑥(𝑦 = 𝑤𝜑) ↔ (𝑦 = 𝑤 → ∀𝑥𝜑))
32albii 1821 . . . . . 6 (∀𝑦𝑥(𝑦 = 𝑤𝜑) ↔ ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑))
4 alcom 2160 . . . . . 6 (∀𝑦𝑥(𝑦 = 𝑤𝜑) ↔ ∀𝑥𝑦(𝑦 = 𝑤𝜑))
53, 4bitr3i 280 . . . . 5 (∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑) ↔ ∀𝑥𝑦(𝑦 = 𝑤𝜑))
65imbi2i 339 . . . 4 ((𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)) ↔ (𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
76albii 1821 . . 3 (∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)) ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
8 df-sb 2070 . . 3 ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)))
9 19.21v 1940 . . . 4 (∀𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)) ↔ (𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
109albii 1821 . . 3 (∀𝑤𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)) ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
117, 8, 103bitr4i 306 . 2 ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑤𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
12 df-sb 2070 . . 3 ([𝑧 / 𝑦]𝜑 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
1312albii 1821 . 2 (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
141, 11, 133bitr4i 306 1 ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  [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-11 2158 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-sb 2070 This theorem is referenced by:  sbalv  2164  sbcal  3782  ax11-pm2  34425  bj-sbnf  34430  ichal  44151
 Copyright terms: Public domain W3C validator