Theorem sb5ALTVD 39149

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 2430, 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 38731 is sb5ALTVD 39149 without virtual deductions and was automatically derived from sb5ALTVD 39149.

1::	|- (. [ y / x ] ph ->. [ y / x ] ph ).
2::	|- [ y / x ] x = y
3:1,2:	|- (. [ y / x ] ph ->. [ y / x ] ( x = y /\ ph ) ).
4:3:	|- (. [ y / x ] ph ->. E. x ( x = y /\ ph ) ).
5:4:	|- ( [ y / x ] ph -> E. x ( x = y /\ ph ) )
6::	|- (. E. x ( x = y /\ ph ) ->. E. x ( x = y /\ ph ) ).
7::	|- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. ( x = y /\ ph ) ).
8:7:	|- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. ph ).
9:7:	|- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. x = y ).
10:8,9:	|- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. [ y / x ] ph ).
101::	|- ( [ y / x ] ph -> A. x [ y / x ] ph )
11:101,10:	|- ( E. x ( x = y /\ ph ) -> [ y / x ] ph )
12:5,11:	|- ( ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) /\ ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) )
qed:12:	|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
sb5ALTVD	|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem sb5ALTVD

Step	Hyp	Ref	Expression
1		idn1 38790	. . . . . 6 |- (. [ y / x ] ph ->. [ y / x ] ph ).
2		equsb1 2368	. . . . . 6 |- [ y / x ] x = y
3		sban 2399	. . . . . . 7 |- ( [ y / x ] ( x = y /\ ph ) <-> ( [ y / x ] x = y /\ [ y / x ] ph ) )
4	3	simplbi2com 657	. . . . . 6 |- ( [ y / x ] ph -> ( [ y / x ] x = y -> [ y / x ] ( x = y /\ ph ) ) )
5	1, 2, 4	e10 38919	. . . . 5 |- (. [ y / x ] ph ->. [ y / x ] ( x = y /\ ph ) ).
6		spsbe 1884	. . . . 5 |- ( [ y / x ] ( x = y /\ ph ) -> E. x ( x = y /\ ph ) )
7	5, 6	e1a 38852	. . . 4 |- (. [ y / x ] ph ->. E. x ( x = y /\ ph ) ).
8	7	in1 38787	. . 3 |- ( [ y / x ] ph -> E. x ( x = y /\ ph ) )
9		hbs1 2436	. . . 4 |- ( [ y / x ] ph -> A. x [ y / x ] ph )
10		idn2 38838	. . . . . 6 |- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. ( x = y /\ ph ) ).
11		simpr 477	. . . . . 6 |- ( ( x = y /\ ph ) -> ph )
12	10, 11	e2 38856	. . . . 5 |- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. ph ).
13		simpl 473	. . . . . 6 |- ( ( x = y /\ ph ) -> x = y )
14	10, 13	e2 38856	. . . . 5 |- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. x = y ).
15		sbequ1 2110	. . . . . 6 |- ( x = y -> ( ph -> [ y / x ] ph ) )
16	15	com12 32	. . . . 5 |- ( ph -> ( x = y -> [ y / x ] ph ) )
17	12, 14, 16	e22 38896	. . . 4 |- (. E. x ( x = y /\ ph ) ,. ( x = y /\ ph ) ->. [ y / x ] ph ).
18	9, 17	exinst 38849	. . 3 |- ( E. x ( x = y /\ ph ) -> [ y / x ] ph )
19	8, 18	pm3.2i 471	. 2 |- ( ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) /\ ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) )
20		impbi 198	. . 3 |- ( ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) -> ( ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) -> ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) ) )
21	20	imp 445	. 2 |- ( ( ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) /\ ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) ) -> ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) )
22	19, 21	e0a 38999	1 |- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881  df-vd1 38786  df-vd2 38794

This theorem is referenced by: (None)