![]() |
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 2273, 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 41231 is sb5ALTVD 41619 without virtual deductions and
was automatically derived from sb5ALTVD 41619.
|
Ref | Expression |
---|---|
sb5ALTVD | ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 41280 | . . . . . 6 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥]𝜑 ) | |
2 | equsb1 2509 | . . . . . 6 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
3 | sban 2085 | . . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑)) | |
4 | 3 | simplbi2com 506 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑))) |
5 | 1, 2, 4 | e10 41400 | . . . . 5 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ) |
6 | spsbe 2087 | . . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
7 | 5, 6 | e1a 41333 | . . . 4 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ) |
8 | 7 | in1 41277 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
9 | hbs1 2271 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
10 | idn2 41319 | . . . . . 6 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ (𝑥 = 𝑦 ∧ 𝜑) ) | |
11 | simpr 488 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑) | |
12 | 10, 11 | e2 41337 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝜑 ) |
13 | simpl 486 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦) | |
14 | 10, 13 | e2 41337 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝑥 = 𝑦 ) |
15 | sbequ1 2246 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
16 | 15 | com12 32 | . . . . 5 ⊢ (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑)) |
17 | 12, 14, 16 | e22 41377 | . . . 4 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ [𝑦 / 𝑥]𝜑 ) |
18 | 9, 17 | exinst 41330 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) |
19 | 8, 18 | pm3.2i 474 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) |
20 | impbi 211 | . . 3 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ((∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))) | |
21 | 20 | imp 410 | . 2 ⊢ ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
22 | 19, 21 | e0a 41478 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∃wex 1781 [wsb 2069 |
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 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-12 2175 ax-13 2379 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-sb 2070 df-vd1 41276 df-vd2 41284 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |