Theorem sb5ALTVD 44401

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 2262, 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 44013 is sb5ALTVD 44401 without virtual deductions and was automatically derived from sb5ALTVD 44401.

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

Step	Hyp	Ref	Expression
1		idn1 44062	. . . . . 6 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2		equsb1 2485	. . . . . 6 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
3		sban 2075	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑))
4	3	simplbi2com 501	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)))
5	1, 2, 4	e10 44182	. . . . 5 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)   )
6		spsbe 2077	. . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
7	5, 6	e1a 44115	. . . 4 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   )
8	7	in1 44059	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
9		hbs1 2260	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
10		idn2 44101	. . . . . 6 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   (𝑥 = 𝑦 ∧ 𝜑)   )
11		simpr 483	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑)
12	10, 11	e2 44119	. . . . 5 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   𝜑   )
13		simpl 481	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦)
14	10, 13	e2 44119	. . . . 5 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   𝑥 = 𝑦   )
15		sbequ1 2235	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
16	15	com12 32	. . . . 5 ⊢ (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑))
17	12, 14, 16	e22 44159	. . . 4 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   [𝑦 / 𝑥]𝜑   )
18	9, 17	exinst 44112	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)
19	8, 18	pm3.2i 469	. 2 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
20		impbi 207	. . 3 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ((∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))))
21	20	imp 405	. 2 ⊢ ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
22	19, 21	e0a 44260	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533  ∃wex 1773  [wsb 2059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-12 2166  ax-13 2366

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778  df-sb 2060  df-vd1 44058  df-vd2 44066

This theorem is referenced by: (None)