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

Theorem sbal2 2549
 Description: Move quantifier in and out of substitution. Usage of this theorem is discouraged because it depends on ax-13 2379. Check out sbal 2163 for a version replacing the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022.) (Proof shortened by Wolf Lammen, 23-Sep-2023.) (New usage is discouraged.)
Assertion
Ref Expression
sbal2 (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Distinct variable group:   𝑥,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem sbal2
StepHypRef Expression
1 sbequ12 2250 . . . . 5 (𝑦 = 𝑧 → (∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑))
21sps 2182 . . . 4 (∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑))
3 sbequ12 2250 . . . . . 6 (𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑))
43sps 2182 . . . . 5 (∀𝑦 𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑))
54dral2 2449 . . . 4 (∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
62, 5bitr3d 284 . . 3 (∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
76adantl 485 . 2 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
8 sb4b 2488 . . . 4 (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑)))
98adantl 485 . . 3 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑)))
10 nfnae 2445 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑧
11 sb4b 2488 . . . . . 6 (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧𝜑)))
1210, 11albid 2222 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥𝑦(𝑦 = 𝑧𝜑)))
13 alcom 2160 . . . . 5 (∀𝑥𝑦(𝑦 = 𝑧𝜑) ↔ ∀𝑦𝑥(𝑦 = 𝑧𝜑))
1412, 13syl6bb 290 . . . 4 (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑦𝑥(𝑦 = 𝑧𝜑)))
15 nfnae 2445 . . . . 5 𝑦 ¬ ∀𝑥 𝑥 = 𝑦
16 nfeqf1 2386 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧)
17 19.21t 2204 . . . . . 6 (Ⅎ𝑥 𝑦 = 𝑧 → (∀𝑥(𝑦 = 𝑧𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑)))
1816, 17syl 17 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑥(𝑦 = 𝑧𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑)))
1915, 18albid 2222 . . . 4 (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑦𝑥(𝑦 = 𝑧𝜑) ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑)))
2014, 19sylan9bbr 514 . . 3 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑)))
219, 20bitr4d 285 . 2 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
227, 21pm2.61dan 812 1 (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀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 2142  ax-11 2158  ax-12 2175  ax-13 2379 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070 This theorem is referenced by:  2sb5ndVD  41787  2sb5ndALT  41809
 Copyright terms: Public domain W3C validator