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

Theorem ifeqeqx 28161
Description: An equality theorem tailored for ballotlemsf1o 29355. (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 2437 . 2  |-  ( A  =  if ( ch ,  A ,  B
)  ->  ( a  =  A  <->  a  =  if ( ch ,  A ,  B ) ) )
2 eqeq2 2437 . 2  |-  ( B  =  if ( ch ,  A ,  B
)  ->  ( a  =  B  <->  a  =  if ( ch ,  A ,  B ) ) )
3 simplr 760 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
4 simpll 758 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ph )
5 simpr 462 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ch )
6 sbceq1a 3310 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
76biimpd 210 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch ) )
83, 5, 7sylc 62 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch )
9 dfsbcq 3301 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( [. X  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
10 csbeq1 3398 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1110eqeq2d 2436 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
129, 11imbi12d 321 . . . . 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 3301 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( [. Y  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
14 csbeq1 3398 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1514eqeq2d 2436 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
1613, 15imbi12d 321 . . . . 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 2581 . . . . . . . . . . 11  |-  ( X  e.  W  ->  F/_ x C )
19 ifeqeqx.1 . . . . . . . . . . 11  |-  ( x  =  X  ->  A  =  C )
2018, 19csbiegf 3419 . . . . . . . . . 10  |-  ( X  e.  W  ->  [_ X  /  x ]_ A  =  C )
2117, 20syl 17 . . . . . . . . 9  |-  ( ph  ->  [_ X  /  x ]_ A  =  C
)
22 ifeqeqx.5 . . . . . . . . 9  |-  ( ph  ->  a  =  C )
2321, 22eqtr4d 2466 . . . . . . . 8  |-  ( ph  ->  [_ X  /  x ]_ A  =  a
)
2423adantr 466 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  [_ X  /  x ]_ A  =  a
)
2524eqcomd 2430 . . . . . 6  |-  ( (
ph  /\  ps )  ->  a  =  [_ X  /  x ]_ A )
2625a1d 26 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ A ) )
27 pm3.24 890 . . . . . . . . . 10  |-  -.  ( ps  /\  -.  ps )
28 ifeqeqx.y . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  V )
29 ifeqeqx.4 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  ( ch 
<->  ps ) )
3029sbcieg 3332 . . . . . . . . . . . 12  |-  ( Y  e.  V  ->  ( [. Y  /  x ]. ch  <->  ps ) )
3128, 30syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( [. Y  /  x ]. ch  <->  ps )
)
3231anbi1d 709 . . . . . . . . . 10  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  <->  ( ps  /\ 
-.  ps ) ) )
3327, 32mtbiri 304 . . . . . . . . 9  |-  ( ph  ->  -.  ( [. Y  /  x ]. ch  /\  -.  ps ) )
3433pm2.21d 109 . . . . . . . 8  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ A ) )
3534imp 430 . . . . . . 7  |-  ( (
ph  /\  ( [. Y  /  x ]. ch  /\ 
-.  ps ) )  -> 
a  =  [_ Y  /  x ]_ A )
3635anass1rs 814 . . . . . 6  |-  ( ( ( ph  /\  -.  ps )  /\  [. Y  /  x ]. ch )  ->  a  =  [_ Y  /  x ]_ A )
3736ex 435 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ A ) )
3812, 16, 26, 37ifbothda 3946 . . . 4  |-  ( ph  ->  ( [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
394, 8, 38sylc 62 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
40 csbeq1a 3404 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
4140eqeq2d 2436 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
4241biimprd 226 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ A  ->  a  =  A ) )
433, 39, 42sylc 62 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  A )
44 simplr 760 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
45 simpll 758 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  ph )
46 simpr 462 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  ch )
476notbid 295 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
4847biimpd 210 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
4944, 46, 48sylc 62 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch )
509notbid 295 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. X  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
51 csbeq1 3398 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
5251eqeq2d 2436 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
5350, 52imbi12d 321 . . . . 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 295 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. Y  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
55 csbeq1 3398 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
5655eqeq2d 2436 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
5754, 56imbi12d 321 . . . . 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 3332 . . . . . . . . . . . . 13  |-  ( X  e.  W  ->  ( [. X  /  x ]. ch  <->  th ) )
6017, 59syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( [. X  /  x ]. ch  <->  th )
)
6160notbid 295 . . . . . . . . . . 11  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  <->  -.  th )
)
6261biimpd 210 . . . . . . . . . 10  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
th ) )
63 ifeqeqx.6 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  th )
6463ex 435 . . . . . . . . . 10  |-  ( ph  ->  ( ps  ->  th )
)
6562, 64nsyld 145 . . . . . . . . 9  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
ps ) )
6665anim2d 567 . . . . . . . 8  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  ( ps  /\  -.  ps )
) )
6727, 66mtoi 181 . . . . . . 7  |-  ( ph  ->  -.  ( ps  /\  -.  [. X  /  x ]. ch ) )
6867pm2.21d 109 . . . . . 6  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  a  =  [_ X  /  x ]_ B ) )
6968expdimp 438 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( -.  [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ B ) )
70 nfcvd 2581 . . . . . . . . . 10  |-  ( Y  e.  V  ->  F/_ x
a )
71 ifeqeqx.2 . . . . . . . . . 10  |-  ( x  =  Y  ->  B  =  a )
7270, 71csbiegf 3419 . . . . . . . . 9  |-  ( Y  e.  V  ->  [_ Y  /  x ]_ B  =  a )
7328, 72syl 17 . . . . . . . 8  |-  ( ph  ->  [_ Y  /  x ]_ B  =  a
)
7473adantr 466 . . . . . . 7  |-  ( (
ph  /\  -.  ps )  ->  [_ Y  /  x ]_ B  =  a
)
7574eqcomd 2430 . . . . . 6  |-  ( (
ph  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ B )
7675a1d 26 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( -.  [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ B ) )
7753, 57, 69, 76ifbothda 3946 . . . 4  |-  ( ph  ->  ( -.  [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
7845, 49, 77sylc 62 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
79 csbeq1a 3404 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
8079eqeq2d 2436 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
8180biimprd 226 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ B  ->  a  =  B ) )
8244, 78, 81sylc 62 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  B )
831, 2, 43, 82ifbothda 3946 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 187    /\ wa 370    = wceq 1437    e. wcel 1872   [.wsbc 3299   [_csb 3395   ifcif 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-sbc 3300  df-csb 3396  df-if 3912
This theorem is referenced by:  ballotlemsf1o  29355  ballotlemsf1oOLD  29393
  Copyright terms: Public domain W3C validator