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

Theorem sbal 2158
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 2155 . 2 (∀𝑤𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)) ↔ ∀𝑥𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
2 19.21v 1933 . . . . . . 7 (∀𝑥(𝑦 = 𝑤𝜑) ↔ (𝑦 = 𝑤 → ∀𝑥𝜑))
32albii 1813 . . . . . 6 (∀𝑦𝑥(𝑦 = 𝑤𝜑) ↔ ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑))
4 alcom 2155 . . . . . 6 (∀𝑦𝑥(𝑦 = 𝑤𝜑) ↔ ∀𝑥𝑦(𝑦 = 𝑤𝜑))
53, 4bitr3i 278 . . . . 5 (∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑) ↔ ∀𝑥𝑦(𝑦 = 𝑤𝜑))
65imbi2i 337 . . . 4 ((𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)) ↔ (𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
76albii 1813 . . 3 (∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)) ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
8 df-sb 2063 . . 3 ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → ∀𝑥𝜑)))
9 19.21v 1933 . . . 4 (∀𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)) ↔ (𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
109albii 1813 . . 3 (∀𝑤𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)) ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑥𝑦(𝑦 = 𝑤𝜑)))
117, 8, 103bitr4i 304 . 2 ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑤𝑥(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
12 df-sb 2063 . . 3 ([𝑧 / 𝑦]𝜑 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
1312albii 1813 . 2 (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜑)))
141, 11, 133bitr4i 304 1 ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1528  [wsb 2062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-11 2153
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-sb 2063
This theorem is referenced by:  sbalv  2159  sbcal  3836  ax11-pm2  34046  bj-sbnf  34051  ichal  43462
  Copyright terms: Public domain W3C validator