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 2276, 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 40879 is sb5ALTVD 41267 without virtual deductions and
was automatically derived from sb5ALTVD 41267.
|
Ref | Expression |
---|---|
sb5ALTVD | ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 40928 | . . . . . 6 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥]𝜑 ) | |
2 | equsb1 2530 | . . . . . 6 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
3 | sban 2086 | . . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑)) | |
4 | 3 | simplbi2com 505 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑))) |
5 | 1, 2, 4 | e10 41048 | . . . . 5 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ) |
6 | spsbe 2088 | . . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | |
7 | 5, 6 | e1a 40981 | . . . 4 ⊢ ( [𝑦 / 𝑥]𝜑 ▶ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ) |
8 | 7 | in1 40925 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
9 | hbs1 2274 | . . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | |
10 | idn2 40967 | . . . . . 6 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ (𝑥 = 𝑦 ∧ 𝜑) ) | |
11 | simpr 487 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑) | |
12 | 10, 11 | e2 40985 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝜑 ) |
13 | simpl 485 | . . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦) | |
14 | 10, 13 | e2 40985 | . . . . 5 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ 𝑥 = 𝑦 ) |
15 | sbequ1 2249 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
16 | 15 | com12 32 | . . . . 5 ⊢ (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑)) |
17 | 12, 14, 16 | e22 41025 | . . . 4 ⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑) ▶ [𝑦 / 𝑥]𝜑 ) |
18 | 9, 17 | exinst 40978 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) |
19 | 8, 18 | pm3.2i 473 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) |
20 | impbi 210 | . . 3 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ((∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))) | |
21 | 20 | imp 409 | . 2 ⊢ ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
22 | 19, 21 | e0a 41126 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∃wex 1780 [wsb 2069 |
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 1911 ax-6 1970 ax-7 2015 ax-10 2145 ax-12 2177 ax-13 2390 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-nf 1785 df-sb 2070 df-vd1 40924 df-vd2 40932 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |