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

Theorem sb5ALTVD 41567
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 2278, 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 41179 is sb5ALTVD 41567 without virtual deductions and was automatically derived from sb5ALTVD 41567.
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 41228 . . . . . 6 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2 equsb1 2532 . . . . . 6 [𝑦 / 𝑥]𝑥 = 𝑦
3 sban 2087 . . . . . . 7 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑))
43simplbi2com 506 . . . . . 6 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦𝜑)))
51, 2, 4e10 41348 . . . . 5 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦𝜑)   )
6 spsbe 2089 . . . . 5 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6e1a 41281 . . . 4 (   [𝑦 / 𝑥]𝜑   ▶   𝑥(𝑥 = 𝑦𝜑)   )
87in1 41225 . . 3 ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑))
9 hbs1 2276 . . . 4 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
10 idn2 41267 . . . . . 6 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   (𝑥 = 𝑦𝜑)   )
11 simpr 488 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝜑)
1210, 11e2 41285 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝜑   )
13 simpl 486 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝑥 = 𝑦)
1410, 13e2 41285 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝑥 = 𝑦   )
15 sbequ1 2251 . . . . . 6 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
1615com12 32 . . . . 5 (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑))
1712, 14, 16e22 41325 . . . 4 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   [𝑦 / 𝑥]𝜑   )
189, 17exinst 41278 . . 3 (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
198, 18pm3.2i 474 . 2 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑))
20 impbi 211 . . 3 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) → ((∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))))
2120imp 410 . 2 ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑)))
2219, 21e0a 41426 1 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wex 1781  [wsb 2070
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 1912  ax-6 1971  ax-7 2016  ax-10 2146  ax-12 2179  ax-13 2392
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-vd1 41224  df-vd2 41232
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator