Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-sbcom2d Structured version   Unicode version

Theorem wl-sbcom2d 31378
Description: Version of sbcom2 2213 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
Hypotheses
Ref Expression
wl-sbcom2d.1  |-  ( ph  ->  -.  A. x  x  =  w )
wl-sbcom2d.2  |-  ( ph  ->  -.  A. x  x  =  z )
wl-sbcom2d.3  |-  ( ph  ->  -.  A. z  z  =  y )
Assertion
Ref Expression
wl-sbcom2d  |-  ( ph  ->  ( [ w  / 
z ] [ y  /  x ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) )

Proof of Theorem wl-sbcom2d
Dummy variables  v  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax6ev 1773 . 2  |-  E. u  u  =  y
2 ax6ev 1773 . 2  |-  E. v 
v  =  w
3 wl-sbcom2d.2 . . . . . . . 8  |-  ( ph  ->  -.  A. x  x  =  z )
4 wl-sbcom2d-lem2 31377 . . . . . . . . . . 11  |-  ( -. 
A. z  z  =  x  ->  ( [
u  /  x ] [ v  /  z ] ps  <->  A. x A. z
( ( x  =  u  /\  z  =  v )  ->  ps ) ) )
5 alcom 1869 . . . . . . . . . . . 12  |-  ( A. x A. z ( ( x  =  u  /\  z  =  v )  ->  ps )  <->  A. z A. x ( ( x  =  u  /\  z  =  v )  ->  ps ) )
6 ancomst 450 . . . . . . . . . . . . 13  |-  ( ( ( x  =  u  /\  z  =  v )  ->  ps )  <->  ( ( z  =  v  /\  x  =  u )  ->  ps )
)
762albii 1662 . . . . . . . . . . . 12  |-  ( A. z A. x ( ( x  =  u  /\  z  =  v )  ->  ps )  <->  A. z A. x ( ( z  =  v  /\  x  =  u )  ->  ps ) )
85, 7bitri 249 . . . . . . . . . . 11  |-  ( A. x A. z ( ( x  =  u  /\  z  =  v )  ->  ps )  <->  A. z A. x ( ( z  =  v  /\  x  =  u )  ->  ps ) )
94, 8syl6bb 261 . . . . . . . . . 10  |-  ( -. 
A. z  z  =  x  ->  ( [
u  /  x ] [ v  /  z ] ps  <->  A. z A. x
( ( z  =  v  /\  x  =  u )  ->  ps ) ) )
109naecoms 2079 . . . . . . . . 9  |-  ( -. 
A. x  x  =  z  ->  ( [
u  /  x ] [ v  /  z ] ps  <->  A. z A. x
( ( z  =  v  /\  x  =  u )  ->  ps ) ) )
11 wl-sbcom2d-lem2 31377 . . . . . . . . 9  |-  ( -. 
A. x  x  =  z  ->  ( [
v  /  z ] [ u  /  x ] ps  <->  A. z A. x
( ( z  =  v  /\  x  =  u )  ->  ps ) ) )
1210, 11bitr4d 256 . . . . . . . 8  |-  ( -. 
A. x  x  =  z  ->  ( [
u  /  x ] [ v  /  z ] ps  <->  [ v  /  z ] [ u  /  x ] ps ) )
133, 12syl 17 . . . . . . 7  |-  ( ph  ->  ( [ u  /  x ] [ v  / 
z ] ps  <->  [ v  /  z ] [
u  /  x ] ps ) )
1413adantl 464 . . . . . 6  |-  ( ( ( u  =  y  /\  v  =  w )  /\  ph )  ->  ( [ u  /  x ] [ v  / 
z ] ps  <->  [ v  /  z ] [
u  /  x ] ps ) )
15 wl-sbcom2d.1 . . . . . . . 8  |-  ( ph  ->  -.  A. x  x  =  w )
16 wl-sbcom2d-lem1 31376 . . . . . . . 8  |-  ( ( u  =  y  /\  v  =  w )  ->  ( -.  A. x  x  =  w  ->  ( [ u  /  x ] [ v  /  z ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) ) )
1715, 16syl5 30 . . . . . . 7  |-  ( ( u  =  y  /\  v  =  w )  ->  ( ph  ->  ( [ u  /  x ] [ v  /  z ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) ) )
1817imp 427 . . . . . 6  |-  ( ( ( u  =  y  /\  v  =  w )  /\  ph )  ->  ( [ u  /  x ] [ v  / 
z ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) )
19 wl-sbcom2d.3 . . . . . . . . 9  |-  ( ph  ->  -.  A. z  z  =  y )
20 wl-sbcom2d-lem1 31376 . . . . . . . . 9  |-  ( ( v  =  w  /\  u  =  y )  ->  ( -.  A. z 
z  =  y  -> 
( [ v  / 
z ] [ u  /  x ] ps  <->  [ w  /  z ] [
y  /  x ] ps ) ) )
2119, 20syl5 30 . . . . . . . 8  |-  ( ( v  =  w  /\  u  =  y )  ->  ( ph  ->  ( [ v  /  z ] [ u  /  x ] ps  <->  [ w  /  z ] [ y  /  x ] ps ) ) )
2221ancoms 451 . . . . . . 7  |-  ( ( u  =  y  /\  v  =  w )  ->  ( ph  ->  ( [ v  /  z ] [ u  /  x ] ps  <->  [ w  /  z ] [ y  /  x ] ps ) ) )
2322imp 427 . . . . . 6  |-  ( ( ( u  =  y  /\  v  =  w )  /\  ph )  ->  ( [ v  / 
z ] [ u  /  x ] ps  <->  [ w  /  z ] [
y  /  x ] ps ) )
2414, 18, 233bitr3rd 284 . . . . 5  |-  ( ( ( u  =  y  /\  v  =  w )  /\  ph )  ->  ( [ w  / 
z ] [ y  /  x ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) )
2524exp31 602 . . . 4  |-  ( u  =  y  ->  (
v  =  w  -> 
( ph  ->  ( [ w  /  z ] [ y  /  x ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) ) ) )
2625exlimdv 1745 . . 3  |-  ( u  =  y  ->  ( E. v  v  =  w  ->  ( ph  ->  ( [ w  /  z ] [ y  /  x ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) ) ) )
2726exlimiv 1743 . 2  |-  ( E. u  u  =  y  ->  ( E. v 
v  =  w  -> 
( ph  ->  ( [ w  /  z ] [ y  /  x ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) ) ) )
281, 2, 27mp2 9 1  |-  ( ph  ->  ( [ w  / 
z ] [ y  /  x ] ps  <->  [ y  /  x ] [ w  /  z ] ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367   A.wal 1403   E.wex 1633   [wsb 1763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1634  df-nf 1638  df-sb 1764
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator