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

Theorem 2sb5ndALT 28220
Description: Equivalence for double substitution 2sb5 2084 without distinct  x,  y requirement. 2sb5nd 27820 is derived from 2sb5ndVD 28197. 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 28197. (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 27819 . 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 27812 . . . . . . . . 9  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
43exbii 1573 . . . . . . . 8  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
5 hbs1 2077 . . . . . . . . . . . 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 1924 . . . . . . . . . . . . 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 2077 . . . . . . . . . . . . . 14  |-  ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
1211sbt 2005 . . . . . . . . . . . . 13  |-  [ u  /  x ] ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
13 sbi1 2035 . . . . . . . . . . . . 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 1916 . . . . . . . . . . . . . . 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 2106 . . . . . . . . . . . . 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 27829 . . . . . . . . . . . 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 1542 . . . . . . . . 9  |-  F/ y [ u  /  x ] [ v  /  y ] ph
262519.41 1846 . . . . . . . 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 1573 . . . . . 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 2078 . . . . . . 7  |-  F/ x [ u  /  x ] [ v  /  y ] ph
302919.41 1846 . . . . . 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 1531   E.wex 1532    = wceq 1633   [wsb 1639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-ne 2481  df-v 2824
  Copyright terms: Public domain W3C validator