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

Theorem 2sb5ndALT 29044
Description: Equivalence for double substitution 2sb5 2188 without distinct  x,  y requirement. 2sb5nd 28647 is derived from 2sb5ndVD 29022. 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 29022. (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 28646 . 2  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
2 anabs5 785 . . . 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 28639 . . . . . . . . 9  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
43exbii 1592 . . . . . . . 8  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
5 hbs1 2181 . . . . . . . . . . . 12  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. x [ u  /  x ] [ v  /  y ] ph )
6 id 20 . . . . . . . . . . . . 13  |-  ( A. x  x  =  y  ->  A. x  x  =  y )
7 ax10o 2038 . . . . . . . . . . . . 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 569 . . . . . . . . . . . 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 645 . . . . . . . . . . 11  |-  ( A. x  x  =  y  ->  ( [ u  /  x ] [ v  / 
y ] ph  ->  A. y [ u  /  x ] [ v  / 
y ] ph )
)
11 hbs1 2181 . . . . . . . . . . . . . 14  |-  ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
1211sbt 2126 . . . . . . . . . . . . 13  |-  [ u  /  x ] ( [ v  /  y ]
ph  ->  A. y [ v  /  y ] ph )
13 sbi1 2132 . . . . . . . . . . . . 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 20 . . . . . . . . . . . . . 14  |-  ( -. 
A. x  x  =  y  ->  -.  A. x  x  =  y )
16 ax10 2025 . . . . . . . . . . . . . . 15  |-  ( A. y  y  =  x  ->  A. x  x  =  y )
1716con3i 129 . . . . . . . . . . . . . 14  |-  ( -. 
A. x  x  =  y  ->  -.  A. y 
y  =  x )
1815, 17syl 16 . . . . . . . . . . . . 13  |-  ( -. 
A. x  x  =  y  ->  -.  A. y 
y  =  x )
19 sbal2 2211 . . . . . . . . . . . . 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 315 . . . . . . . . . . . . 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 28656 . . . . . . . . . . . 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 645 . . . . . . . . . . 11  |-  ( -. 
A. x  x  =  y  ->  ( [
u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
2410, 23pm2.61i 158 . . . . . . . . . 10  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph )
2524nfi 1560 . . . . . . . . 9  |-  F/ y [ u  /  x ] [ v  /  y ] ph
262519.41 1900 . . . . . . . 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 243 . . . . . . 7  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  <->  ( E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
2827exbii 1592 . . . . . 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 2182 . . . . . . 7  |-  F/ x [ u  /  x ] [ v  /  y ] ph
302919.41 1900 . . . . . 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 242 . . . . 5  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) 
<->  E. x E. y
( ( x  =  u  /\  y  =  v )  /\  ph ) )
3231anbi2i 676 . . . 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 243 . . 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 618 . . 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 201 . 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 188 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 177    \/ wo 358    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652   [wsb 1658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-ne 2601  df-v 2958
  Copyright terms: Public domain W3C validator