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

Theorem sb5ALTVD 28734
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 2149, 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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sb5ALT 28320 is sb5ALTVD 28734 without virtual deductions and was automatically derived from sb5ALTVD 28734.
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 28374 . . . . . 6  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ph ).
2 equsb1 2083 . . . . . 6  |-  [ y  /  x ] x  =  y
3 sban 2118 . . . . . . 7  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  <->  ( [
y  /  x ]
x  =  y  /\  [ y  /  x ] ph ) )
43simplbi2com 1380 . . . . . 6  |-  ( [ y  /  x ] ph  ->  ( [ y  /  x ] x  =  y  ->  [ y  /  x ] ( x  =  y  /\  ph ) ) )
51, 2, 4e10 28504 . . . . 5  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ( x  =  y  /\  ph ) ).
6 spsbe 2124 . . . . 5  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  ->  E. x ( x  =  y  /\  ph )
)
75, 6e1_ 28437 . . . 4  |-  (. [
y  /  x ] ph  ->.  E. x ( x  =  y  /\  ph ) ).
87in1 28371 . . 3  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph ) )
9 hbs1 2154 . . . 4  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
10 idn2 28423 . . . . . 6  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ( x  =  y  /\  ph ) ).
11 simpr 448 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  ph )
1210, 11e2 28441 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ph ).
13 simpl 444 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  x  =  y )
1410, 13e2 28441 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  x  =  y ).
15 sbequ1 1939 . . . . . 6  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
1615com12 29 . . . . 5  |-  ( ph  ->  ( x  =  y  ->  [ y  /  x ] ph ) )
1712, 14, 16e22 28481 . . . 4  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  [ y  /  x ] ph ).
189, 17exinst 28434 . . 3  |-  ( E. x ( x  =  y  /\  ph )  ->  [ y  /  x ] ph )
198, 18pm3.2i 442 . 2  |-  ( ( [ y  /  x ] ph  ->  E. x
( x  =  y  /\  ph ) )  /\  ( E. x
( x  =  y  /\  ph )  ->  [ y  /  x ] ph ) )
20 bi3 180 . . 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 419 . 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, 21e0_ 28593 1  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649   [wsb 1655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-vd1 28370  df-vd2 28379
  Copyright terms: Public domain W3C validator