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

Theorem 2sb5ndALT 29025
Description: Equivalence for double substitution 2sb5 2064 without distinct  x,  y requirement. 2sb5nd 28625 is derived from 2sb5ndVD 29002. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD 29002. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
2sb5ndALT  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  -> 
( [ u  /  x ] [ v  / 
y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
Distinct variable groups:    x, u    y, u    x, v    y,
v
Allowed substitution hints:    ph( x, y, v, u)

Proof of Theorem 2sb5ndALT
StepHypRef Expression
1 a9e2ndeq 28624 . 2  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
2 anabs5 784 . . . 4  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  /\  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
3 2pm13.193 28617 . . . . . . . . 9  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
43exbii 1572 . . . . . . . 8  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
5 hbs1 2057 . . . . . . . . . . . 12  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. x [ u  /  x ] [ v  /  y ] ph )
6 id 19 . . . . . . . . . . . . 13  |-  ( A. x  x  =  y  ->  A. x  x  =  y )
7 ax10o 1905 . . . . . . . . . . . . 13  |-  ( A. x  x  =  y  ->  ( A. x [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
86, 7syl 15 . . . . . . . . . . . 12  |-  ( A. x  x  =  y  ->  ( A. x [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
9 pm3.33 568 . . . . . . . . . . . 12  |-  ( ( ( [ u  /  x ] [ v  / 
y ] ph  ->  A. x [ u  /  x ] [ v  / 
y ] ph )  /\  ( A. x [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )  -> 
( [ u  /  x ] [ v  / 
y ] ph  ->  A. y [ u  /  x ] [ v  / 
y ] ph )
)
105, 8, 9sylancr 644 . . . . . . . . . . 11  |-  ( A. x  x  =  y  ->  ( [ u  /  x ] [ v  / 
y ] ph  ->  A. y [ u  /  x ] [ v  / 
y ] ph )
)
11 hbs1 2057 . . . . . . . . . . . . . 14  |-  ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
1211sbt 1986 . . . . . . . . . . . . 13  |-  [ u  /  x ] ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
13 sbi1 2016 . . . . . . . . . . . . 13  |-  ( [ u  /  x ]
( [ v  / 
y ] ph  ->  A. y [ v  / 
y ] ph )  ->  ( [ u  /  x ] [ v  / 
y ] ph  ->  [ u  /  x ] A. y [ v  / 
y ] ph )
)
1412, 13ax-mp 8 . . . . . . . . . . . 12  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  [ u  /  x ] A. y [ v  /  y ] ph )
15 id 19 . . . . . . . . . . . . . 14  |-  ( -. 
A. x  x  =  y  ->  -.  A. x  x  =  y )
16 ax10 1897 . . . . . . . . . . . . . . 15  |-  ( A. y  y  =  x  ->  A. x  x  =  y )
1716con3i 127 . . . . . . . . . . . . . 14  |-  ( -. 
A. x  x  =  y  ->  -.  A. y 
y  =  x )
1815, 17syl 15 . . . . . . . . . . . . 13  |-  ( -. 
A. x  x  =  y  ->  -.  A. y 
y  =  x )
19 sbal2 2086 . . . . . . . . . . . . 13  |-  ( -. 
A. y  y  =  x  ->  ( [
u  /  x ] A. y [ v  / 
y ] ph  <->  A. y [ u  /  x ] [ v  /  y ] ph ) )
2018, 19syl 15 . . . . . . . . . . . 12  |-  ( -. 
A. x  x  =  y  ->  ( [
u  /  x ] A. y [ v  / 
y ] ph  <->  A. y [ u  /  x ] [ v  /  y ] ph ) )
21 imbi2 314 . . . . . . . . . . . . 13  |-  ( ( [ u  /  x ] A. y [ v  /  y ] ph  <->  A. y [ u  /  x ] [ v  / 
y ] ph )  ->  ( ( [ u  /  x ] [ v  /  y ] ph  ->  [ u  /  x ] A. y [ v  /  y ] ph ) 
<->  ( [ u  /  x ] [ v  / 
y ] ph  ->  A. y [ u  /  x ] [ v  / 
y ] ph )
) )
2221biimpa21 28634 . . . . . . . . . . . 12  |-  ( ( ( [ u  /  x ] [ v  / 
y ] ph  ->  [ u  /  x ] A. y [ v  / 
y ] ph )  /\  ( [ u  /  x ] A. y [ v  /  y ]
ph 
<-> 
A. y [ u  /  x ] [ v  /  y ] ph ) )  ->  ( [ u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
2314, 20, 22sylancr 644 . . . . . . . . . . 11  |-  ( -. 
A. x  x  =  y  ->  ( [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
2410, 23pm2.61i 156 . . . . . . . . . 10  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph )
2524nfi 1541 . . . . . . . . 9  |-  F/ y [ u  /  x ] [ v  /  y ] ph
262519.41 1827 . . . . . . . 8  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  ( E. y ( x  =  u  /\  y  =  v )  /\  [
u  /  x ] [ v  /  y ] ph ) )
274, 26bitr3i 242 . . . . . . 7  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  <->  ( E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
2827exbii 1572 . . . . . 6  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  <->  E. x ( E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
29 nfs1v 2058 . . . . . . 7  |-  F/ x [ u  /  x ] [ v  /  y ] ph
302919.41 1827 . . . . . 6  |-  ( E. x ( E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [
u  /  x ] [ v  /  y ] ph ) )
3128, 30bitr2i 241 . . . . 5  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
3231anbi2i 675 . . . 4  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  /\  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )
) )
332, 32bitr3i 242 . . 3  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
34 pm5.32 617 . . 3  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  ->  ( [
u  /  x ] [ v  /  y ] ph  <->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) ) )  <->  ( ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )
) ) )
3533, 34mpbir 200 . 2  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( [ u  /  x ] [ v  / 
y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
361, 35sylbi 187 1  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  -> 
( [ u  /  x ] [ v  / 
y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358   A.wal 1530   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  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ne 2461  df-v 2803
  Copyright terms: Public domain W3C validator