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

Theorem sb5ALTVD 37349
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 2269, 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 36925 is sb5ALTVD 37349 without virtual deductions and was automatically derived from sb5ALTVD 37349.
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 36986 . . . . . 6  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ph ).
2 equsb1 2207 . . . . . 6  |-  [ y  /  x ] x  =  y
3 sban 2238 . . . . . . 7  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  <->  ( [
y  /  x ]
x  =  y  /\  [ y  /  x ] ph ) )
43simplbi2com 637 . . . . . 6  |-  ( [ y  /  x ] ph  ->  ( [ y  /  x ] x  =  y  ->  [ y  /  x ] ( x  =  y  /\  ph ) ) )
51, 2, 4e10 37115 . . . . 5  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ( x  =  y  /\  ph ) ).
6 spsbe 1811 . . . . 5  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  ->  E. x ( x  =  y  /\  ph )
)
75, 6e1a 37048 . . . 4  |-  (. [
y  /  x ] ph  ->.  E. x ( x  =  y  /\  ph ) ).
87in1 36983 . . 3  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph ) )
9 hbs1 2275 . . . 4  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
10 idn2 37034 . . . . . 6  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ( x  =  y  /\  ph ) ).
11 simpr 467 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  ph )
1210, 11e2 37052 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ph ).
13 simpl 463 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  x  =  y )
1410, 13e2 37052 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  x  =  y ).
15 sbequ1 2092 . . . . . 6  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
1615com12 32 . . . . 5  |-  ( ph  ->  ( x  =  y  ->  [ y  /  x ] ph ) )
1712, 14, 16e22 37092 . . . 4  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  [ y  /  x ] ph ).
189, 17exinst 37045 . . 3  |-  ( E. x ( x  =  y  /\  ph )  ->  [ y  /  x ] ph )
198, 18pm3.2i 461 . 2  |-  ( ( [ y  /  x ] ph  ->  E. x
( x  =  y  /\  ph ) )  /\  ( E. x
( x  =  y  /\  ph )  ->  [ y  /  x ] ph ) )
20 impbi 191 . . 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 435 . 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 37198 1  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1454   E.wex 1673   [wsb 1807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1674  df-nf 1678  df-sb 1808  df-vd1 36982  df-vd2 36990
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator