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

Theorem ifeqeqx 24003
Description: An equality theorem tailored for ballotlemsf1o 24773 (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 2447 . 2  |-  ( A  =  if ( ch ,  A ,  B
)  ->  ( a  =  A  <->  a  =  if ( ch ,  A ,  B ) ) )
2 eqeq2 2447 . 2  |-  ( B  =  if ( ch ,  A ,  B
)  ->  ( a  =  B  <->  a  =  if ( ch ,  A ,  B ) ) )
3 simplr 733 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
4 simpll 732 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ph )
5 simpr 449 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ch )
6 sbceq1a 3173 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
76biimpd 200 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch ) )
83, 5, 7sylc 59 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch )
9 dfsbcq 3165 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( [. X  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
10 csbeq1 3256 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1110eqeq2d 2449 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
129, 11imbi12d 313 . . . . 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 3165 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( [. Y  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
14 csbeq1 3256 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1514eqeq2d 2449 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
1613, 15imbi12d 313 . . . . 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 2575 . . . . . . . . . . 11  |-  ( X  e.  W  ->  F/_ x C )
19 ifeqeqx.1 . . . . . . . . . . 11  |-  ( x  =  X  ->  A  =  C )
2018, 19csbiegf 3293 . . . . . . . . . 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 2473 . . . . . . . 8  |-  ( ph  ->  [_ X  /  x ]_ A  =  a
)
2423adantr 453 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  [_ X  /  x ]_ A  =  a
)
2524eqcomd 2443 . . . . . 6  |-  ( (
ph  /\  ps )  ->  a  =  [_ X  /  x ]_ A )
2625a1d 24 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ A ) )
27 pm3.24 854 . . . . . . . . . 10  |-  -.  ( ps  /\  -.  ps )
28 ifeqeqx.y . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  V )
29 ifeqeqx.4 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  ( ch 
<->  ps ) )
3029sbcieg 3195 . . . . . . . . . . . 12  |-  ( Y  e.  V  ->  ( [. Y  /  x ]. ch  <->  ps ) )
3128, 30syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( [. Y  /  x ]. ch  <->  ps )
)
3231anbi1d 687 . . . . . . . . . 10  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  <->  ( ps  /\ 
-.  ps ) ) )
3327, 32mtbiri 296 . . . . . . . . 9  |-  ( ph  ->  -.  ( [. Y  /  x ]. ch  /\  -.  ps ) )
3433pm2.21d 101 . . . . . . . 8  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ A ) )
3534imp 420 . . . . . . 7  |-  ( (
ph  /\  ( [. Y  /  x ]. ch  /\ 
-.  ps ) )  -> 
a  =  [_ Y  /  x ]_ A )
3635anass1rs 784 . . . . . 6  |-  ( ( ( ph  /\  -.  ps )  /\  [. Y  /  x ]. ch )  ->  a  =  [_ Y  /  x ]_ A )
3736ex 425 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ A ) )
3812, 16, 26, 37ifbothda 3771 . . . 4  |-  ( ph  ->  ( [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
394, 8, 38sylc 59 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
40 csbeq1a 3261 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
4140eqeq2d 2449 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
4241biimprd 216 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ A  ->  a  =  A ) )
433, 39, 42sylc 59 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  A )
44 simplr 733 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
45 simpll 732 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  ph )
46 simpr 449 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  ch )
476notbid 287 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
4847biimpd 200 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
4944, 46, 48sylc 59 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch )
509notbid 287 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. X  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
51 csbeq1 3256 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
5251eqeq2d 2449 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
5350, 52imbi12d 313 . . . . 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 287 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. Y  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
55 csbeq1 3256 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
5655eqeq2d 2449 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
5754, 56imbi12d 313 . . . . 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 3195 . . . . . . . . . . . . 13  |-  ( X  e.  W  ->  ( [. X  /  x ]. ch  <->  th ) )
6017, 59syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( [. X  /  x ]. ch  <->  th )
)
6160notbid 287 . . . . . . . . . . 11  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  <->  -.  th )
)
6261biimpd 200 . . . . . . . . . 10  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
th ) )
63 ifeqeqx.6 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  th )
6463ex 425 . . . . . . . . . 10  |-  ( ph  ->  ( ps  ->  th )
)
6562, 64nsyld 135 . . . . . . . . 9  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
ps ) )
6665anim2d 550 . . . . . . . 8  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  ( ps  /\  -.  ps )
) )
6727, 66mtoi 172 . . . . . . 7  |-  ( ph  ->  -.  ( ps  /\  -.  [. X  /  x ]. ch ) )
6867pm2.21d 101 . . . . . 6  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  a  =  [_ X  /  x ]_ B ) )
6968expdimp 428 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( -.  [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ B ) )
70 nfcvd 2575 . . . . . . . . . 10  |-  ( Y  e.  V  ->  F/_ x
a )
71 ifeqeqx.2 . . . . . . . . . 10  |-  ( x  =  Y  ->  B  =  a )
7270, 71csbiegf 3293 . . . . . . . . 9  |-  ( Y  e.  V  ->  [_ Y  /  x ]_ B  =  a )
7328, 72syl 16 . . . . . . . 8  |-  ( ph  ->  [_ Y  /  x ]_ B  =  a
)
7473adantr 453 . . . . . . 7  |-  ( (
ph  /\  -.  ps )  ->  [_ Y  /  x ]_ B  =  a
)
7574eqcomd 2443 . . . . . 6  |-  ( (
ph  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ B )
7675a1d 24 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( -.  [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ B ) )
7753, 57, 69, 76ifbothda 3771 . . . 4  |-  ( ph  ->  ( -.  [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
7845, 49, 77sylc 59 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
79 csbeq1a 3261 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
8079eqeq2d 2449 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
8180biimprd 216 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ B  ->  a  =  B ) )
8244, 78, 81sylc 59 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  B )
831, 2, 43, 82ifbothda 3771 1  |-  ( (
ph  /\  x  =  if ( ps ,  X ,  Y ) )  -> 
a  =  if ( ch ,  A ,  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   [.wsbc 3163   [_csb 3253   ifcif 3741
This theorem is referenced by:  ballotlemsf1o  24773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-sbc 3164  df-csb 3254  df-if 3742
  Copyright terms: Public domain W3C validator