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 43989
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 2266, 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 43601 is sb5ALTVD 43989 without virtual deductions and was automatically derived from sb5ALTVD 43989.
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 43650 . . . . . 6 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2 equsb1 2489 . . . . . 6 [𝑦 / 𝑥]𝑥 = 𝑦
3 sban 2082 . . . . . . 7 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑))
43simplbi2com 502 . . . . . 6 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦𝜑)))
51, 2, 4e10 43770 . . . . 5 (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦𝜑)   )
6 spsbe 2084 . . . . 5 ([𝑦 / 𝑥](𝑥 = 𝑦𝜑) → ∃𝑥(𝑥 = 𝑦𝜑))
75, 6e1a 43703 . . . 4 (   [𝑦 / 𝑥]𝜑   ▶   𝑥(𝑥 = 𝑦𝜑)   )
87in1 43647 . . 3 ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑))
9 hbs1 2264 . . . 4 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
10 idn2 43689 . . . . . 6 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   (𝑥 = 𝑦𝜑)   )
11 simpr 484 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝜑)
1210, 11e2 43707 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝜑   )
13 simpl 482 . . . . . 6 ((𝑥 = 𝑦𝜑) → 𝑥 = 𝑦)
1410, 13e2 43707 . . . . 5 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   𝑥 = 𝑦   )
15 sbequ1 2239 . . . . . 6 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
1615com12 32 . . . . 5 (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑))
1712, 14, 16e22 43747 . . . 4 (   𝑥(𝑥 = 𝑦𝜑)   ,   (𝑥 = 𝑦𝜑)   ▶   [𝑦 / 𝑥]𝜑   )
189, 17exinst 43700 . . 3 (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)
198, 18pm3.2i 470 . 2 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑))
20 impbi 207 . . 3 (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) → ((∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))))
2120imp 406 . 2 ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦𝜑)) ∧ (∃𝑥(𝑥 = 𝑦𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑)))
2219, 21e0a 43848 1 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1540  wex 1780  [wsb 2066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-10 2136  ax-12 2170  ax-13 2370
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1781  df-nf 1785  df-sb 2067  df-vd1 43646  df-vd2 43654
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator