Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2sb5ndALT Structured version   Visualization version   GIF version

Theorem 2sb5ndALT 41633
Description: Equivalence for double substitution 2sb5 2278 without distinct 𝑥, 𝑦 requirement. 2sb5nd 41261 is derived from 2sb5ndVD 41611. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD 41611. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
2sb5ndALT ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣   𝑦,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem 2sb5ndALT
StepHypRef Expression
1 ax6e2ndeq 41260 . 2 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) ↔ ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
2 anabs5 662 . . . 4 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3 2pm13.193 41253 . . . . . . . . 9 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
43exbii 1849 . . . . . . . 8 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
5 hbs1 2271 . . . . . . . . . . . 12 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
6 id 22 . . . . . . . . . . . . 13 (∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
7 axc11 2441 . . . . . . . . . . . . 13 (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
86, 7syl 17 . . . . . . . . . . . 12 (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
9 pm3.33 764 . . . . . . . . . . . 12 ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ∧ (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
105, 8, 9sylancr 590 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
11 hbs1 2271 . . . . . . . . . . . . . 14 ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
1211sbt 2071 . . . . . . . . . . . . 13 [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
13 sbi1 2076 . . . . . . . . . . . . 13 ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑))
1412, 13ax-mp 5 . . . . . . . . . . . 12 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑)
15 id 22 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
16 axc11n 2437 . . . . . . . . . . . . . . 15 (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
1716con3i 157 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
1815, 17syl 17 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
19 sbal2 2549 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2018, 19syl 17 . . . . . . . . . . . 12 (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
21 imbi2 352 . . . . . . . . . . . . 13 (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
2221biimpac 482 . . . . . . . . . . . 12 ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ∧ ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2314, 20, 22sylancr 590 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2410, 23pm2.61i 185 . . . . . . . . . 10 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
2524nf5i 2147 . . . . . . . . 9 𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
262519.41 2235 . . . . . . . 8 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
274, 26bitr3i 280 . . . . . . 7 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2827exbii 1849 . . . . . 6 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
29 nfs1v 2157 . . . . . . 7 𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
302919.41 2235 . . . . . 6 (∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3128, 30bitr2i 279 . . . . 5 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
3231anbi2i 625 . . . 4 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
332, 32bitr3i 280 . . 3 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
34 pm5.32 577 . . 3 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))))
3533, 34mpbir 234 . 2 (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
361, 35sylbi 220 1 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  wal 1536   = wceq 1538  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-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379  ax-ext 2770
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  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator