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

Theorem 2sb5ndALT 34133
Description: Equivalence for double substitution 2sb5 2189 without distinct  x,  y requirement. 2sb5nd 33727 is derived from 2sb5ndVD 34111. 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 34111. (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 33726 . 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 33719 . . . . . . . . 9  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
43exbii 1672 . . . . . . . 8  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
5 hbs1 2182 . . . . . . . . . . . 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 2058 . . . . . . . . . . . . 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 583 . . . . . . . . . . . 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 661 . . . . . . . . . . 11  |-  ( A. x  x  =  y  ->  ( [ u  /  x ] [ v  / 
y ] ph  ->  A. y [ u  /  x ] [ v  / 
y ] ph )
)
11 hbs1 2182 . . . . . . . . . . . . . 14  |-  ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
1211sbt 2164 . . . . . . . . . . . . 13  |-  [ u  /  x ] ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
13 sbi1 2135 . . . . . . . . . . . . 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 2053 . . . . . . . . . . . . . . 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 2207 . . . . . . . . . . . . 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 322 . . . . . . . . . . . . 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 33736 . . . . . . . . . . . 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 661 . . . . . . . . . . 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 1628 . . . . . . . . 9  |-  F/ y [ u  /  x ] [ v  /  y ] ph
262519.41 1976 . . . . . . . 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 1672 . . . . . 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 2183 . . . . . . 7  |-  F/ x [ u  /  x ] [ v  /  y ] ph
302919.41 1976 . . . . . 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 692 . . . 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 634 . . 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 366    /\ wa 367   A.wal 1396    = wceq 1398   E.wex 1617   [wsb 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ne 2651  df-v 3108
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator