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

Theorem 2sb5ndALT 32001
Description: Equivalence for double substitution 2sb5 2158 without distinct  x,  y requirement. 2sb5nd 31602 is derived from 2sb5ndVD 31979. 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 31979. (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 ax6e2ndeq 31601 . 2  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
2 anabs5 807 . . . 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 31594 . . . . . . . . 9  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
43exbii 1635 . . . . . . . 8  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
5 hbs1 2150 . . . . . . . . . . . 12  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. x [ u  /  x ] [ v  /  y ] ph )
6 id 22 . . . . . . . . . . . . 13  |-  ( A. x  x  =  y  ->  A. x  x  =  y )
7 axc11 2014 . . . . . . . . . . . . 13  |-  ( A. x  x  =  y  ->  ( A. x [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
86, 7syl 16 . . . . . . . . . . . 12  |-  ( A. x  x  =  y  ->  ( A. x [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
9 pm3.33 585 . . . . . . . . . . . 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 663 . . . . . . . . . . 11  |-  ( A. x  x  =  y  ->  ( [ u  /  x ] [ v  / 
y ] ph  ->  A. y [ u  /  x ] [ v  / 
y ] ph )
)
11 hbs1 2150 . . . . . . . . . . . . . 14  |-  ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
1211sbt 2127 . . . . . . . . . . . . 13  |-  [ u  /  x ] ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
13 sbi1 2094 . . . . . . . . . . . . 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 5 . . . . . . . . . . . 12  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  [ u  /  x ] A. y [ v  /  y ] ph )
15 id 22 . . . . . . . . . . . . . 14  |-  ( -. 
A. x  x  =  y  ->  -.  A. x  x  =  y )
16 axc11n 2009 . . . . . . . . . . . . . . 15  |-  ( A. y  y  =  x  ->  A. x  x  =  y )
1716con3i 135 . . . . . . . . . . . . . 14  |-  ( -. 
A. x  x  =  y  ->  -.  A. y 
y  =  x )
1815, 17syl 16 . . . . . . . . . . . . 13  |-  ( -. 
A. x  x  =  y  ->  -.  A. y 
y  =  x )
19 sbal2 2182 . . . . . . . . . . . . 13  |-  ( -. 
A. y  y  =  x  ->  ( [
u  /  x ] A. y [ v  / 
y ] ph  <->  A. y [ u  /  x ] [ v  /  y ] ph ) )
2018, 19syl 16 . . . . . . . . . . . 12  |-  ( -. 
A. x  x  =  y  ->  ( [
u  /  x ] A. y [ v  / 
y ] ph  <->  A. y [ u  /  x ] [ v  /  y ] ph ) )
21 imbi2 324 . . . . . . . . . . . . 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 31611 . . . . . . . . . . . 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 663 . . . . . . . . . . 11  |-  ( -. 
A. x  x  =  y  ->  ( [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
2410, 23pm2.61i 164 . . . . . . . . . 10  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph )
2524nfi 1597 . . . . . . . . 9  |-  F/ y [ u  /  x ] [ v  /  y ] ph
262519.41 1911 . . . . . . . 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 251 . . . . . . 7  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  <->  ( E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
2827exbii 1635 . . . . . 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 2151 . . . . . . 7  |-  F/ x [ u  /  x ] [ v  /  y ] ph
302919.41 1911 . . . . . 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 250 . . . . 5  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
3231anbi2i 694 . . . 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 251 . . 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 636 . . 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 209 . 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 195 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369   A.wal 1368    = wceq 1370   E.wex 1587   [wsb 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ne 2650  df-v 3080
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator