Mathbox for Wolf Lammen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-2sb6d Structured version   Visualization version   GIF version

Theorem wl-2sb6d 32520
 Description: Version of 2sb6 2432 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
Hypotheses
Ref Expression
wl-2sb6d.1 (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)
wl-2sb6d.2 (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)
wl-2sb6d.3 (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)
wl-2sb6d.4 (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)
Assertion
Ref Expression
wl-2sb6d (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥𝑦((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓)))

Proof of Theorem wl-2sb6d
StepHypRef Expression
1 wl-2sb6d.4 . 2 (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)
2 wl-2sb6d.2 . 2 (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)
3 wl-2sb6d.1 . . 3 (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)
4 wl-2sb6d.3 . . 3 (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)
53, 4jca 553 . 2 (𝜑 → (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
6 wl-sb6nae 32518 . . 3 (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥(𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓)))
7 nfnae 2306 . . . . 5 𝑥 ¬ ∀𝑦 𝑦 = 𝑤
8 wl-nfnae1 32495 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑥
9 nfnae 2306 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑧
108, 9nfan 1816 . . . . 5 𝑥(¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
117, 10nfan 1816 . . . 4 𝑥(¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
12 wl-sb6nae 32518 . . . . . 6 (¬ ∀𝑦 𝑦 = 𝑤 → ([𝑤 / 𝑦]𝜓 ↔ ∀𝑦(𝑦 = 𝑤𝜓)))
1312imbi2d 329 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑤 → ((𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓) ↔ (𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜓))))
14 impexp 461 . . . . . . 7 (((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓) ↔ (𝑥 = 𝑧 → (𝑦 = 𝑤𝜓)))
1514albii 1737 . . . . . 6 (∀𝑦((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓) ↔ ∀𝑦(𝑥 = 𝑧 → (𝑦 = 𝑤𝜓)))
16 nfeqf 2289 . . . . . . 7 ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑥 = 𝑧)
17 19.21t 2061 . . . . . . 7 (Ⅎ𝑦 𝑥 = 𝑧 → (∀𝑦(𝑥 = 𝑧 → (𝑦 = 𝑤𝜓)) ↔ (𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜓))))
1816, 17syl 17 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑦(𝑥 = 𝑧 → (𝑦 = 𝑤𝜓)) ↔ (𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜓))))
1915, 18syl5rbb 272 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ((𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤𝜓)) ↔ ∀𝑦((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓)))
2013, 19sylan9bb 732 . . . 4 ((¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧)) → ((𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓) ↔ ∀𝑦((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓)))
2111, 20albid 2077 . . 3 ((¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧)) → (∀𝑥(𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓) ↔ ∀𝑥𝑦((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓)))
226, 21sylan9bb 732 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧))) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥𝑦((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓)))
231, 2, 5, 22syl12anc 1316 1 (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥𝑦((𝑥 = 𝑧𝑦 = 𝑤) → 𝜓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  Ⅎwnf 1699  [wsb 1867 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868 This theorem is referenced by:  wl-sbcom2d-lem2  32522
 Copyright terms: Public domain W3C validator