Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifeqeqx Structured version   Unicode version

Theorem ifeqeqx 25902
Description: An equality theorem tailored for ballotlemsf1o 26896 (Contributed by Thierry Arnoux, 14-Apr-2017.)
Hypotheses
Ref Expression
ifeqeqx.1  |-  ( x  =  X  ->  A  =  C )
ifeqeqx.2  |-  ( x  =  Y  ->  B  =  a )
ifeqeqx.3  |-  ( x  =  X  ->  ( ch 
<->  th ) )
ifeqeqx.4  |-  ( x  =  Y  ->  ( ch 
<->  ps ) )
ifeqeqx.5  |-  ( ph  ->  a  =  C )
ifeqeqx.6  |-  ( (
ph  /\  ps )  ->  th )
ifeqeqx.y  |-  ( ph  ->  Y  e.  V )
ifeqeqx.x  |-  ( ph  ->  X  e.  W )
Assertion
Ref Expression
ifeqeqx  |-  ( (
ph  /\  x  =  if ( ps ,  X ,  Y ) )  -> 
a  =  if ( ch ,  A ,  B ) )
Distinct variable groups:    x, a    x, C    x, X    x, Y    x, V    x, W    ps, x    th, x
Allowed substitution hints:    ph( x, a)    ps( a)    ch( x, a)    th( a)    A( x, a)    B( x, a)    C( a)    V( a)    W( a)    X( a)    Y( a)

Proof of Theorem ifeqeqx
StepHypRef Expression
1 eqeq2 2452 . 2  |-  ( A  =  if ( ch ,  A ,  B
)  ->  ( a  =  A  <->  a  =  if ( ch ,  A ,  B ) ) )
2 eqeq2 2452 . 2  |-  ( B  =  if ( ch ,  A ,  B
)  ->  ( a  =  B  <->  a  =  if ( ch ,  A ,  B ) ) )
3 simplr 754 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
4 simpll 753 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ph )
5 simpr 461 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ch )
6 sbceq1a 3197 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
76biimpd 207 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch ) )
83, 5, 7sylc 60 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch )
9 dfsbcq 3188 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( [. X  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
10 csbeq1 3291 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1110eqeq2d 2454 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
129, 11imbi12d 320 . . . . 5  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( ( [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ A )  <->  ( [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) ) )
13 dfsbcq 3188 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( [. Y  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
14 csbeq1 3291 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1514eqeq2d 2454 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
1613, 15imbi12d 320 . . . . 5  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( ( [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ A )  <->  ( [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) ) )
17 ifeqeqx.x . . . . . . . . . 10  |-  ( ph  ->  X  e.  W )
18 nfcvd 2580 . . . . . . . . . . 11  |-  ( X  e.  W  ->  F/_ x C )
19 ifeqeqx.1 . . . . . . . . . . 11  |-  ( x  =  X  ->  A  =  C )
2018, 19csbiegf 3312 . . . . . . . . . 10  |-  ( X  e.  W  ->  [_ X  /  x ]_ A  =  C )
2117, 20syl 16 . . . . . . . . 9  |-  ( ph  ->  [_ X  /  x ]_ A  =  C
)
22 ifeqeqx.5 . . . . . . . . 9  |-  ( ph  ->  a  =  C )
2321, 22eqtr4d 2478 . . . . . . . 8  |-  ( ph  ->  [_ X  /  x ]_ A  =  a
)
2423adantr 465 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  [_ X  /  x ]_ A  =  a
)
2524eqcomd 2448 . . . . . 6  |-  ( (
ph  /\  ps )  ->  a  =  [_ X  /  x ]_ A )
2625a1d 25 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ A ) )
27 pm3.24 877 . . . . . . . . . 10  |-  -.  ( ps  /\  -.  ps )
28 ifeqeqx.y . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  V )
29 ifeqeqx.4 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  ( ch 
<->  ps ) )
3029sbcieg 3219 . . . . . . . . . . . 12  |-  ( Y  e.  V  ->  ( [. Y  /  x ]. ch  <->  ps ) )
3128, 30syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( [. Y  /  x ]. ch  <->  ps )
)
3231anbi1d 704 . . . . . . . . . 10  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  <->  ( ps  /\ 
-.  ps ) ) )
3327, 32mtbiri 303 . . . . . . . . 9  |-  ( ph  ->  -.  ( [. Y  /  x ]. ch  /\  -.  ps ) )
3433pm2.21d 106 . . . . . . . 8  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ A ) )
3534imp 429 . . . . . . 7  |-  ( (
ph  /\  ( [. Y  /  x ]. ch  /\ 
-.  ps ) )  -> 
a  =  [_ Y  /  x ]_ A )
3635anass1rs 805 . . . . . 6  |-  ( ( ( ph  /\  -.  ps )  /\  [. Y  /  x ]. ch )  ->  a  =  [_ Y  /  x ]_ A )
3736ex 434 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ A ) )
3812, 16, 26, 37ifbothda 3824 . . . 4  |-  ( ph  ->  ( [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
394, 8, 38sylc 60 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
40 csbeq1a 3297 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
4140eqeq2d 2454 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
4241biimprd 223 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ A  ->  a  =  A ) )
433, 39, 42sylc 60 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  A )
44 simplr 754 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
45 simpll 753 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  ph )
46 simpr 461 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  ch )
476notbid 294 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
4847biimpd 207 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
4944, 46, 48sylc 60 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch )
509notbid 294 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. X  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
51 csbeq1 3291 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
5251eqeq2d 2454 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
5350, 52imbi12d 320 . . . . 5  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( ( -.  [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ B )  <->  ( -.  [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) ) )
5413notbid 294 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. Y  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
55 csbeq1 3291 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
5655eqeq2d 2454 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
5754, 56imbi12d 320 . . . . 5  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( ( -.  [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ B )  <->  ( -.  [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) ) )
58 ifeqeqx.3 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  ( ch 
<->  th ) )
5958sbcieg 3219 . . . . . . . . . . . . 13  |-  ( X  e.  W  ->  ( [. X  /  x ]. ch  <->  th ) )
6017, 59syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( [. X  /  x ]. ch  <->  th )
)
6160notbid 294 . . . . . . . . . . 11  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  <->  -.  th )
)
6261biimpd 207 . . . . . . . . . 10  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
th ) )
63 ifeqeqx.6 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  th )
6463ex 434 . . . . . . . . . 10  |-  ( ph  ->  ( ps  ->  th )
)
6562, 64nsyld 140 . . . . . . . . 9  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
ps ) )
6665anim2d 565 . . . . . . . 8  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  ( ps  /\  -.  ps )
) )
6727, 66mtoi 178 . . . . . . 7  |-  ( ph  ->  -.  ( ps  /\  -.  [. X  /  x ]. ch ) )
6867pm2.21d 106 . . . . . 6  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  a  =  [_ X  /  x ]_ B ) )
6968expdimp 437 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( -.  [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ B ) )
70 nfcvd 2580 . . . . . . . . . 10  |-  ( Y  e.  V  ->  F/_ x
a )
71 ifeqeqx.2 . . . . . . . . . 10  |-  ( x  =  Y  ->  B  =  a )
7270, 71csbiegf 3312 . . . . . . . . 9  |-  ( Y  e.  V  ->  [_ Y  /  x ]_ B  =  a )
7328, 72syl 16 . . . . . . . 8  |-  ( ph  ->  [_ Y  /  x ]_ B  =  a
)
7473adantr 465 . . . . . . 7  |-  ( (
ph  /\  -.  ps )  ->  [_ Y  /  x ]_ B  =  a
)
7574eqcomd 2448 . . . . . 6  |-  ( (
ph  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ B )
7675a1d 25 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( -.  [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ B ) )
7753, 57, 69, 76ifbothda 3824 . . . 4  |-  ( ph  ->  ( -.  [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
7845, 49, 77sylc 60 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
79 csbeq1a 3297 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
8079eqeq2d 2454 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
8180biimprd 223 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ B  ->  a  =  B ) )
8244, 78, 81sylc 60 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  B )
831, 2, 43, 82ifbothda 3824 1  |-  ( (
ph  /\  x  =  if ( ps ,  X ,  Y ) )  -> 
a  =  if ( ch ,  A ,  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   [.wsbc 3186   [_csb 3288   ifcif 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-sbc 3187  df-csb 3289  df-if 3792
This theorem is referenced by:  ballotlemsf1o  26896
  Copyright terms: Public domain W3C validator