![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sb5ALTVD | Structured version Visualization version GIF version |
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 2251, 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 39685 is sb5ALTVD 40082 without virtual deductions and
was automatically derived from sb5ALTVD 40082.
|
Ref | Expression |
---|---|
sb5ALTVD | ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 39734 | . . . . . 6 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥]𝜑 ) | |
2 | equsb1 2444 | . . . . . 6 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
3 | sban 2475 | . . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑)) | |
4 | 3 | simplbi2com 498 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑))) |
5 | 1, 2, 4 | e10 39863 | . . . . 5 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ) |
6 | spsbe 2015 | . . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
7 | 5, 6 | e1a 39796 | . . . 4 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ) |
8 | 7 | in1 39731 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
9 | hbs1 2255 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
10 | idn2 39782 | . . . . . 6 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ (𝑥 = 𝑦 ∧ 𝜑) ) | |
11 | simpr 479 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑) | |
12 | 10, 11 | e2 39800 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝜑 ) |
13 | simpl 476 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦) | |
14 | 10, 13 | e2 39800 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝑥 = 𝑦 ) |
15 | sbequ1 2228 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
16 | 15 | com12 32 | . . . . 5 ⊢ (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑)) |
17 | 12, 14, 16 | e22 39840 | . . . 4 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ [𝑦 / 𝑥]𝜑 ) |
18 | 9, 17 | exinst 39793 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) |
19 | 8, 18 | pm3.2i 464 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) |
20 | impbi 200 | . . 3 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ((∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))) | |
21 | 20 | imp 397 | . 2 ⊢ ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
22 | 19, 21 | e0a 39941 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∃wex 1823 [wsb 2011 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-10 2135 ax-12 2163 ax-13 2334 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-ex 1824 df-nf 1828 df-sb 2012 df-vd1 39730 df-vd2 39738 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |