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

Theorem sb5ALTVD 38068
Description: The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 20 Excercise 3.a., which is sb5 2322, found in the "Answers to Starred Exercises" on page 457 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sb5ALT 37649 is sb5ALTVD 38068 without virtual deductions and was automatically derived from sb5ALTVD 38068.
 1:: ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   ) 2:: ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 3:1,2: ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)   ) 4:3: ⊢ (   [𝑦 / 𝑥]𝜑   ▶   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑 )   ) 5:4: ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ) 6:: ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ▶   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ) 7:: ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   (𝑥 = 𝑦 ∧ 𝜑)   ) 8:7: ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   𝜑   ) 9:7: ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   𝑥 = 𝑦   ) 10:8,9: ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   [𝑦 / 𝑥]𝜑   ) 101:: ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) 11:101,10: ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑 ) 12:5,11: ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑 )) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) qed:12: ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) )
(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sb5ALTVD ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem sb5ALTVD
StepHypRef Expression
1 idn1 37708 . . . . . 6 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2 equsb1 2260 . . . . . 6 [𝑦 / 𝑥]𝑥 = 𝑦
3 sban 2291 . . . . . . 7 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑))
43simplbi2com 654 . . . . . 6 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦𝜑)))
51, 2, 4e10 37837 . . . . 5 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦𝜑)   )
6 spsbe 1834 . . . . 5 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6e1a 37770 . . . 4 (   [𝑦 / 𝑥]𝜑   ▶   𝑥(𝑥 = 𝑦𝜑)   )
87in1 37705 . . 3 ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑))
9 hbs1 2328 . . . 4 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
10 idn2 37756 . . . . . 6 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   (𝑥 = 𝑦𝜑)   )
11 simpr 475 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝜑)
1210, 11e2 37774 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝜑   )
13 simpl 471 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝑥 = 𝑦)
1410, 13e2 37774 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝑥 = 𝑦   )
15 sbequ1 2129 . . . . . 6 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
1615com12 32 . . . . 5 (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑))
1712, 14, 16e22 37814 . . . 4 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   [𝑦 / 𝑥]𝜑   )
189, 17exinst 37767 . . 3 (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
198, 18pm3.2i 469 . 2 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑))
20 impbi 196 . . 3 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) → ((∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))))
2120imp 443 . 2 ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑)))
2219, 21e0a 37917 1 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   = wceq 1474  ∃wex 1694  [wsb 1830 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-12 1983  ax-13 2137 This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1699  df-sb 1831  df-vd1 37704  df-vd2 37712 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator