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 35242
 Description: Version of sbcom2 2165 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 1972 . 2 𝑢 𝑢 = 𝑦
2 ax6ev 1972 . 2 𝑣 𝑣 = 𝑤
3 wl-sbcom2d.2 . . . . . . . 8 (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)
4 wl-sbcom2d-lem2 35241 . . . . . . . . . . 11 (¬ ∀𝑧 𝑧 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓)))
5 alcom 2160 . . . . . . . . . . . 12 (∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ∀𝑧𝑥((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓))
6 ancomst 468 . . . . . . . . . . . . 13 (((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓))
762albii 1822 . . . . . . . . . . . 12 (∀𝑧𝑥((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓))
85, 7bitri 278 . . . . . . . . . . 11 (∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜓) ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓))
94, 8bitrdi 290 . . . . . . . . . 10 (¬ ∀𝑧 𝑧 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓)))
109naecoms 2440 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓)))
11 wl-sbcom2d-lem2 35241 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜓)))
1210, 11bitr4d 285 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑥]𝜓))
133, 12syl 17 . . . . . . 7 (𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑥]𝜓))
1413adantl 485 . . . . . 6 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑥]𝜓))
15 wl-sbcom2d.1 . . . . . . . 8 (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤)
16 wl-sbcom2d-lem1 35240 . . . . . . . 8 ((𝑢 = 𝑦𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓)))
1715, 16syl5 34 . . . . . . 7 ((𝑢 = 𝑦𝑣 = 𝑤) → (𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓)))
1817imp 410 . . . . . 6 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
19 wl-sbcom2d.3 . . . . . . . . 9 (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦)
20 wl-sbcom2d-lem1 35240 . . . . . . . . 9 ((𝑣 = 𝑤𝑢 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓)))
2119, 20syl5 34 . . . . . . . 8 ((𝑣 = 𝑤𝑢 = 𝑦) → (𝜑 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓)))
2221ancoms 462 . . . . . . 7 ((𝑢 = 𝑦𝑣 = 𝑤) → (𝜑 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓)))
2322imp 410 . . . . . 6 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜓 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜓))
2414, 18, 233bitr3rd 313 . . . . 5 (((𝑢 = 𝑦𝑣 = 𝑤) ∧ 𝜑) → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
2524exp31 423 . . . 4 (𝑢 = 𝑦 → (𝑣 = 𝑤 → (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))))
2625exlimdv 1934 . . 3 (𝑢 = 𝑦 → (∃𝑣 𝑣 = 𝑤 → (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))))
2726exlimiv 1931 . 2 (∃𝑢 𝑢 = 𝑦 → (∃𝑣 𝑣 = 𝑤 → (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))))
281, 2, 27mp2 9 1 (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781  [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: (None)
 Copyright terms: Public domain W3C validator