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 2267, 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 40736 is sb5ALTVD 41124 without virtual deductions and
was automatically derived from sb5ALTVD 41124.
|
Ref | Expression |
---|---|
sb5ALTVD | ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 40785 | . . . . . 6 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥]𝜑 ) | |
2 | equsb1 2523 | . . . . . 6 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
3 | sban 2077 | . . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑)) | |
4 | 3 | simplbi2com 503 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑))) |
5 | 1, 2, 4 | e10 40905 | . . . . 5 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ) |
6 | spsbe 2079 | . . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
7 | 5, 6 | e1a 40838 | . . . 4 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ) |
8 | 7 | in1 40782 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
9 | hbs1 2265 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
10 | idn2 40824 | . . . . . 6 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ (𝑥 = 𝑦 ∧ 𝜑) ) | |
11 | simpr 485 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑) | |
12 | 10, 11 | e2 40842 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝜑 ) |
13 | simpl 483 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦) | |
14 | 10, 13 | e2 40842 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝑥 = 𝑦 ) |
15 | sbequ1 2239 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
16 | 15 | com12 32 | . . . . 5 ⊢ (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑)) |
17 | 12, 14, 16 | e22 40882 | . . . 4 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ [𝑦 / 𝑥]𝜑 ) |
18 | 9, 17 | exinst 40835 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) |
19 | 8, 18 | pm3.2i 471 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) |
20 | impbi 209 | . . 3 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ((∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))) | |
21 | 20 | imp 407 | . 2 ⊢ ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
22 | 19, 21 | e0a 40983 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ∃wex 1771 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-10 2136 ax-12 2167 ax-13 2381 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-nf 1776 df-sb 2061 df-vd1 40781 df-vd2 40789 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |