Theorem sb5ALTVD 45356

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 2287, 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 44969 is sb5ALTVD 45356 without virtual deductions and was automatically derived from sb5ALTVD 45356.

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 45018	. . . . . 6 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2		equsb1 2499	. . . . . 6 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦
3		sban 2091	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) ↔ ([𝑦 / 𝑥]𝑥 = 𝑦 ∧ [𝑦 / 𝑥]𝜑))
4	3	simplbi2com 503	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)))
5	1, 2, 4	e10 45138	. . . . 5 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)   )
6		spsbe 2093	. . . . 5 ⊢ ([𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
7	5, 6	e1a 45071	. . . 4 ⊢ (   [𝑦 / 𝑥]𝜑   ▶   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   )
8	7	in1 45015	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
9		hbs1 2285	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
10		idn2 45057	. . . . . 6 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   (𝑥 = 𝑦 ∧ 𝜑)   )
11		simpr 485	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝜑)
12	10, 11	e2 45075	. . . . 5 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   𝜑   )
13		simpl 483	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦)
14	10, 13	e2 45075	. . . . 5 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   𝑥 = 𝑦   )
15		sbequ1 2260	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
16	15	com12 32	. . . . 5 ⊢ (𝜑 → (𝑥 = 𝑦 → [𝑦 / 𝑥]𝜑))
17	12, 14, 16	e22 45115	. . . 4 ⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑)   ▶   [𝑦 / 𝑥]𝜑   )
18	9, 17	exinst 45068	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)
19	8, 18	pm3.2i 471	. 2 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
20		impbi 209	. . 3 ⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ((∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))))
21	20	imp 407	. 2 ⊢ ((([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
22	19, 21	e0a 45215	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-12 2189  ax-13 2380

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-sb 2074  df-vd1 45014  df-vd2 45022

This theorem is referenced by: (None)