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

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

Proof of Theorem wl-sbcom2d
Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax6ev 1887 . 2 𝑢 𝑢 = 𝑦
2 ax6ev 1887 . 2 𝑣 𝑣 = 𝑤
3 wl-sbcom2d.2 . . . . . . . 8 (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)
4 wl-sbcom2d-lem2 33010 . . . . . . . . . . 11 (¬ ∀𝑧 𝑧 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓)))
5 alcom 2034 . . . . . . . . . . . 12 (∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ∀𝑧𝑥((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓))
6 ancomst 468 . . . . . . . . . . . . 13 (((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓))
762albii 1745 . . . . . . . . . . . 12 (∀𝑧𝑥((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓))
85, 7bitri 264 . . . . . . . . . . 11 (∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓))
94, 8syl6bb 276 . . . . . . . . . 10 (¬ ∀𝑧 𝑧 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓)))
109naecoms 2312 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓)))
11 wl-sbcom2d-lem2 33010 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓)))
1210, 11bitr4d 271 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑥]𝜓))
133, 12syl 17 . . . . . . 7 (𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑥]𝜓))
1413adantl 482 . . . . . 6 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑥]𝜓))
15 wl-sbcom2d.1 . . . . . . . 8 (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤)
16 wl-sbcom2d-lem1 33009 . . . . . . . 8 ((𝑢 = 𝑦𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓)))
1715, 16syl5 34 . . . . . . 7 ((𝑢 = 𝑦𝑣 = 𝑤) → (𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓)))
1817imp 445 . . . . . 6 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
19 wl-sbcom2d.3 . . . . . . . . 9 (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦)
20 wl-sbcom2d-lem1 33009 . . . . . . . . 9 ((𝑣 = 𝑤𝑢 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓)))
2119, 20syl5 34 . . . . . . . 8 ((𝑣 = 𝑤𝑢 = 𝑦) → (𝜑 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓)))
2221ancoms 469 . . . . . . 7 ((𝑢 = 𝑦𝑣 = 𝑤) → (𝜑 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓)))
2322imp 445 . . . . . 6 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓))
2414, 18, 233bitr3rd 299 . . . . 5 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
2524exp31 629 . . . 4 (𝑢 = 𝑦 → (𝑣 = 𝑤 → (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))))
2625exlimdv 1858 . . 3 (𝑢 = 𝑦 → (∃𝑣 𝑣 = 𝑤 → (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))))
2726exlimiv 1855 . 2 (∃𝑢 𝑢 = 𝑦 → (∃𝑣 𝑣 = 𝑤 → (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))))
281, 2, 27mp2 9 1 (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1478  ∃wex 1701  [wsb 1877 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator