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 39702
Description: Equivalence for double substitution 2sb5 2279 without distinct 𝑥, 𝑦 requirement. 2sb5nd 39314 is derived from 2sb5ndVD 39680. 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 39680. (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 39313 . 2 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) ↔ ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
2 anabs5 643 . . . 4 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3 2pm13.193 39306 . . . . . . . . 9 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
43exbii 1927 . . . . . . . 8 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
5 hbs1 2278 . . . . . . . . . . . 12 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
6 id 22 . . . . . . . . . . . . 13 (∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
7 axc11 2469 . . . . . . . . . . . . 13 (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
86, 7syl 17 . . . . . . . . . . . 12 (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
9 pm3.33 770 . . . . . . . . . . . 12 ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ∧ (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
105, 8, 9sylancr 576 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
11 hbs1 2278 . . . . . . . . . . . . . 14 ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
1211sbt 2569 . . . . . . . . . . . . 13 [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
13 sbi1 2542 . . . . . . . . . . . . 13 ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑))
1412, 13ax-mp 5 . . . . . . . . . . . 12 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑)
15 id 22 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
16 axc11n 2465 . . . . . . . . . . . . . . 15 (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
1716con3i 151 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
1815, 17syl 17 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
19 sbal2 2612 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2018, 19syl 17 . . . . . . . . . . . 12 (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
21 imbi2 338 . . . . . . . . . . . . 13 (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
2221biimpac 465 . . . . . . . . . . . 12 ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ∧ ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2314, 20, 22sylancr 576 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2410, 23pm2.61i 176 . . . . . . . . . 10 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
2524nf5i 2182 . . . . . . . . 9 𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
262519.41 2262 . . . . . . . 8 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
274, 26bitr3i 267 . . . . . . 7 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2827exbii 1927 . . . . . 6 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
29 nfs1v 2277 . . . . . . 7 𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
302919.41 2262 . . . . . 6 (∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3128, 30bitr2i 266 . . . . 5 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
3231anbi2i 610 . . . 4 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
332, 32bitr3i 267 . . 3 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
34 pm5.32 564 . . 3 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))))
3533, 34mpbir 222 . 2 (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
361, 35sylbi 208 1 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  wo 863  wal 1632   = wceq 1634  wex 1855  [wsb 2052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-ne 2947  df-v 3357
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator