Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sb5ALTVD Structured version   Unicode version

Theorem sb5ALTVD 33421
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 2158, 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 33003 is sb5ALTVD 33421 without virtual deductions and was automatically derived from sb5ALTVD 33421.
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
StepHypRef Expression
1 idn1 33059 . . . . . 6  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ph ).
2 equsb1 2091 . . . . . 6  |-  [ y  /  x ] x  =  y
3 sban 2124 . . . . . . 7  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  <->  ( [
y  /  x ]
x  =  y  /\  [ y  /  x ] ph ) )
43simplbi2com 627 . . . . . 6  |-  ( [ y  /  x ] ph  ->  ( [ y  /  x ] x  =  y  ->  [ y  /  x ] ( x  =  y  /\  ph ) ) )
51, 2, 4e10 33188 . . . . 5  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ( x  =  y  /\  ph ) ).
6 spsbe 1728 . . . . 5  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  ->  E. x ( x  =  y  /\  ph )
)
75, 6e1a 33121 . . . 4  |-  (. [
y  /  x ] ph  ->.  E. x ( x  =  y  /\  ph ) ).
87in1 33056 . . 3  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph ) )
9 hbs1 2164 . . . 4  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
10 idn2 33107 . . . . . 6  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ( x  =  y  /\  ph ) ).
11 simpr 461 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  ph )
1210, 11e2 33125 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ph ).
13 simpl 457 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  x  =  y )
1410, 13e2 33125 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  x  =  y ).
15 sbequ1 1975 . . . . . 6  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
1615com12 31 . . . . 5  |-  ( ph  ->  ( x  =  y  ->  [ y  /  x ] ph ) )
1712, 14, 16e22 33165 . . . 4  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  [ y  /  x ] ph ).
189, 17exinst 33118 . . 3  |-  ( E. x ( x  =  y  /\  ph )  ->  [ y  /  x ] ph )
198, 18pm3.2i 455 . 2  |-  ( ( [ y  /  x ] ph  ->  E. x
( x  =  y  /\  ph ) )  /\  ( E. x
( x  =  y  /\  ph )  ->  [ y  /  x ] ph ) )
20 bi3 187 . . 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 ) ) ) )
2120imp 429 . 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 ) ) )
2219, 21e0a 33277 1  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1381   E.wex 1597   [wsb 1724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838  ax-13 1983
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1598  df-nf 1602  df-sb 1725  df-vd1 33055  df-vd2 33063
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator