Theorem sb5ALTVD 45512

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 2317, 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 45125 is sb5ALTVD 45512 without virtual deductions and was automatically derived from sb5ALTVD 45512.

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 45174	. . . . . 6 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2		equsb1 2529	. . . . . 6 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
3		sban 2120	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑))
4	3	simplbi2com 507	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)))
5	1, 2, 4	e10 45294	. . . . 5 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)   )
6		spsbe 2122	. . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
7	5, 6	e1a 45227	. . . 4 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   )
8	7	in1 45171	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
9		hbs1 2315	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
10		idn2 45213	. . . . . 6 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   (𝑥 = 𝑦 ∧ 𝜑)   )
11		simpr 489	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑)
12	10, 11	e2 45231	. . . . 5 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   𝜑   )
13		simpl 487	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦)
14	10, 13	e2 45231	. . . . 5 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   𝑥 = 𝑦   )
15		sbequ1 2290	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
16	15	com12 33	. . . . 5 ⊢ (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑))
17	12, 14, 16	e22 45271	. . . 4 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   [𝑦 / 𝑥]𝜑   )
18	9, 17	exinst 45224	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)
19	8, 18	pm3.2i 475	. 2 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
20		impbi 211	. . 3 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ((∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))))
21	20	imp 411	. 2 ⊢ ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
22	19, 21	e0a 45371	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806  [wsb 2097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-12 2219  ax-13 2410

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-sb 2098  df-vd1 45170  df-vd2 45178

This theorem is referenced by: (None)