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

Theorem sb5ALTVD 29005
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 2052, 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 28587 is sb5ALTVD 29005 without virtual deductions and was automatically derived from sb5ALTVD 29005.
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 28641 . . . . . 6  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ph ).
2 equsb1 1987 . . . . . 6  |-  [ y  /  x ] x  =  y
3 sban 2022 . . . . . . 7  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  <->  ( [
y  /  x ]
x  =  y  /\  [ y  /  x ] ph ) )
43simplbi2com 1364 . . . . . 6  |-  ( [ y  /  x ] ph  ->  ( [ y  /  x ] x  =  y  ->  [ y  /  x ] ( x  =  y  /\  ph ) ) )
51, 2, 4e10 28772 . . . . 5  |-  (. [
y  /  x ] ph  ->.  [ y  /  x ] ( x  =  y  /\  ph ) ).
6 spsbe 2028 . . . . 5  |-  ( [ y  /  x ]
( x  =  y  /\  ph )  ->  E. x ( x  =  y  /\  ph )
)
75, 6e1_ 28704 . . . 4  |-  (. [
y  /  x ] ph  ->.  E. x ( x  =  y  /\  ph ) ).
87in1 28638 . . 3  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph ) )
9 hbs1 2057 . . . 4  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
10 idn2 28690 . . . . . 6  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ( x  =  y  /\  ph ) ).
11 simpr 447 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  ph )
1210, 11e2 28708 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  ph ).
13 simpl 443 . . . . . 6  |-  ( ( x  =  y  /\  ph )  ->  x  =  y )
1410, 13e2 28708 . . . . 5  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  x  =  y ).
15 sbequ1 1871 . . . . . 6  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
1615com12 27 . . . . 5  |-  ( ph  ->  ( x  =  y  ->  [ y  /  x ] ph ) )
1712, 14, 16e22 28748 . . . 4  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph )  ->.  [ y  /  x ] ph ).
189, 17exinst 28701 . . 3  |-  ( E. x ( x  =  y  /\  ph )  ->  [ y  /  x ] ph )
198, 18pm3.2i 441 . 2  |-  ( ( [ y  /  x ] ph  ->  E. x
( x  =  y  /\  ph ) )  /\  ( E. x
( x  =  y  /\  ph )  ->  [ y  /  x ] ph ) )
20 bi3 179 . . 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 418 . 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_ 28861 1  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1531    = wceq 1632   [wsb 1638
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-vd1 28637  df-vd2 28646
  Copyright terms: Public domain W3C validator