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 39463
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 2458, 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 39048 is sb5ALTVD 39463 without virtual deductions and was automatically derived from sb5ALTVD 39463.
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 39107 . . . . . 6 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2 equsb1 2396 . . . . . 6 [𝑦 / 𝑥]𝑥 = 𝑦
3 sban 2427 . . . . . . 7 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑))
43simplbi2com 656 . . . . . 6 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦𝜑)))
51, 2, 4e10 39236 . . . . 5 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦𝜑)   )
6 spsbe 1941 . . . . 5 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6e1a 39169 . . . 4 (   [𝑦 / 𝑥]𝜑   ▶   𝑥(𝑥 = 𝑦𝜑)   )
87in1 39104 . . 3 ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑))
9 hbs1 2464 . . . 4 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
10 idn2 39155 . . . . . 6 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   (𝑥 = 𝑦𝜑)   )
11 simpr 476 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝜑)
1210, 11e2 39173 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝜑   )
13 simpl 472 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝑥 = 𝑦)
1410, 13e2 39173 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝑥 = 𝑦   )
15 sbequ1 2148 . . . . . 6 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
1615com12 32 . . . . 5 (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑))
1712, 14, 16e22 39213 . . . 4 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   [𝑦 / 𝑥]𝜑   )
189, 17exinst 39166 . . 3 (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
198, 18pm3.2i 470 . 2 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑))
20 impbi 198 . . 3 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) → ((∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))))
2120imp 444 . 2 ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑)))
2219, 21e0a 39316 1 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wex 1744  [wsb 1937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-sb 1938  df-vd1 39103  df-vd2 39111
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator