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

Theorem ifeqeqx 23034
Description: An equality theorem tailored for ballotlemsf1o 23072 (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 2292 . 2  |-  ( A  =  if ( ch ,  A ,  B
)  ->  ( a  =  A  <->  a  =  if ( ch ,  A ,  B ) ) )
2 eqeq2 2292 . 2  |-  ( B  =  if ( ch ,  A ,  B
)  ->  ( a  =  B  <->  a  =  if ( ch ,  A ,  B ) ) )
3 simplr 731 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
4 simpll 730 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ph )
5 simpr 447 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  ch )
6 sbceq1a 3001 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
76biimpd 198 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( ch  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch ) )
83, 5, 7sylc 56 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  [. if ( ps ,  X ,  Y
)  /  x ]. ch )
9 dfsbcq 2993 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( [. X  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
10 csbeq1 3084 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1110eqeq2d 2294 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
129, 11imbi12d 311 . . . . 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 2993 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( [. Y  /  x ]. ch  <->  [. if ( ps ,  X ,  Y )  /  x ]. ch )
)
14 csbeq1 3084 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
1514eqeq2d 2294 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
1613, 15imbi12d 311 . . . . 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 nfcv 2419 . . . . . . . . . . . 12  |-  F/_ x C
1918a1i 10 . . . . . . . . . . 11  |-  ( X  e.  W  ->  F/_ x C )
20 ifeqeqx.1 . . . . . . . . . . 11  |-  ( x  =  X  ->  A  =  C )
2119, 20csbiegf 3121 . . . . . . . . . 10  |-  ( X  e.  W  ->  [_ X  /  x ]_ A  =  C )
2217, 21syl 15 . . . . . . . . 9  |-  ( ph  ->  [_ X  /  x ]_ A  =  C
)
23 ifeqeqx.5 . . . . . . . . 9  |-  ( ph  ->  a  =  C )
2422, 23eqtr4d 2318 . . . . . . . 8  |-  ( ph  ->  [_ X  /  x ]_ A  =  a
)
2524adantr 451 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  [_ X  /  x ]_ A  =  a
)
2625eqcomd 2288 . . . . . 6  |-  ( (
ph  /\  ps )  ->  a  =  [_ X  /  x ]_ A )
2726a1d 22 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ A ) )
28 simpll 730 . . . . . . 7  |-  ( ( ( ph  /\  -.  ps )  /\  [. Y  /  x ]. ch )  ->  ph )
29 simpr 447 . . . . . . 7  |-  ( ( ( ph  /\  -.  ps )  /\  [. Y  /  x ]. ch )  ->  [. Y  /  x ]. ch )
30 simplr 731 . . . . . . 7  |-  ( ( ( ph  /\  -.  ps )  /\  [. Y  /  x ]. ch )  ->  -.  ps )
31 pm3.24 852 . . . . . . . . . 10  |-  -.  ( ps  /\  -.  ps )
32 ifeqeqx.y . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  V )
33 ifeqeqx.4 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  ( ch 
<->  ps ) )
3433sbcieg 3023 . . . . . . . . . . . 12  |-  ( Y  e.  V  ->  ( [. Y  /  x ]. ch  <->  ps ) )
3532, 34syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( [. Y  /  x ]. ch  <->  ps )
)
3635anbi1d 685 . . . . . . . . . 10  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  <->  ( ps  /\ 
-.  ps ) ) )
3731, 36mtbiri 294 . . . . . . . . 9  |-  ( ph  ->  -.  ( [. Y  /  x ]. ch  /\  -.  ps ) )
3837pm2.21d 98 . . . . . . . 8  |-  ( ph  ->  ( ( [. Y  /  x ]. ch  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ A ) )
3938imp 418 . . . . . . 7  |-  ( (
ph  /\  ( [. Y  /  x ]. ch  /\ 
-.  ps ) )  -> 
a  =  [_ Y  /  x ]_ A )
4028, 29, 30, 39syl12anc 1180 . . . . . 6  |-  ( ( ( ph  /\  -.  ps )  /\  [. Y  /  x ]. ch )  ->  a  =  [_ Y  /  x ]_ A )
4140ex 423 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ A ) )
4212, 16, 27, 41ifbothda 3595 . . . 4  |-  ( ph  ->  ( [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
434, 8, 42sylc 56 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
44 csbeq1a 3089 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  A  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A )
4544eqeq2d 2294 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  A  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ A ) )
4645biimprd 214 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ A  ->  a  =  A ) )
473, 43, 46sylc 56 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  ch )  ->  a  =  A )
48 simplr 731 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  x  =  if ( ps ,  X ,  Y ) )
49 simpll 730 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  ph )
50 simpr 447 . . . . 5  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  ch )
516notbid 285 . . . . . 6  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
5251biimpd 198 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( -.  ch  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
5348, 50, 52sylc 56 . . . 4  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch )
549notbid 285 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. X  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
55 csbeq1 3084 . . . . . . 7  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  [_ X  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
5655eqeq2d 2294 . . . . . 6  |-  ( X  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ X  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
5754, 56imbi12d 311 . . . . 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 ) ) )
5813notbid 285 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( -.  [. Y  /  x ]. ch 
<->  -.  [. if ( ps ,  X ,  Y )  /  x ]. ch ) )
59 csbeq1 3084 . . . . . . 7  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  [_ Y  /  x ]_ B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
6059eqeq2d 2294 . . . . . 6  |-  ( Y  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ Y  /  x ]_ B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
6158, 60imbi12d 311 . . . . 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 ) ) )
62 simpll 730 . . . . . . 7  |-  ( ( ( ph  /\  ps )  /\  -.  [. X  /  x ]. ch )  ->  ph )
63 simplr 731 . . . . . . 7  |-  ( ( ( ph  /\  ps )  /\  -.  [. X  /  x ]. ch )  ->  ps )
64 simpr 447 . . . . . . 7  |-  ( ( ( ph  /\  ps )  /\  -.  [. X  /  x ]. ch )  ->  -.  [. X  /  x ]. ch )
65 ifeqeqx.3 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  ( ch 
<->  th ) )
6665sbcieg 3023 . . . . . . . . . . . . . . 15  |-  ( X  e.  W  ->  ( [. X  /  x ]. ch  <->  th ) )
6717, 66syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( [. X  /  x ]. ch  <->  th )
)
6867notbid 285 . . . . . . . . . . . . 13  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  <->  -.  th )
)
6968biimpd 198 . . . . . . . . . . . 12  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
th ) )
70 ifeqeqx.6 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  th )
7170ex 423 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ps  ->  th )
)
7271con3d 125 . . . . . . . . . . . 12  |-  ( ph  ->  ( -.  th  ->  -. 
ps ) )
7369, 72syld 40 . . . . . . . . . . 11  |-  ( ph  ->  ( -.  [. X  /  x ]. ch  ->  -. 
ps ) )
7473anim2d 548 . . . . . . . . . 10  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  ( ps  /\  -.  ps )
) )
7531, 74mtoi 169 . . . . . . . . 9  |-  ( ph  ->  -.  ( ps  /\  -.  [. X  /  x ]. ch ) )
7675pm2.21d 98 . . . . . . . 8  |-  ( ph  ->  ( ( ps  /\  -.  [. X  /  x ]. ch )  ->  a  =  [_ X  /  x ]_ B ) )
7776imp 418 . . . . . . 7  |-  ( (
ph  /\  ( ps  /\ 
-.  [. X  /  x ]. ch ) )  -> 
a  =  [_ X  /  x ]_ B )
7862, 63, 64, 77syl12anc 1180 . . . . . 6  |-  ( ( ( ph  /\  ps )  /\  -.  [. X  /  x ]. ch )  ->  a  =  [_ X  /  x ]_ B )
7978ex 423 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( -.  [. X  /  x ]. ch  ->  a  =  [_ X  /  x ]_ B ) )
80 nfcvd 2420 . . . . . . . . . 10  |-  ( Y  e.  V  ->  F/_ x
a )
81 ifeqeqx.2 . . . . . . . . . 10  |-  ( x  =  Y  ->  B  =  a )
8280, 81csbiegf 3121 . . . . . . . . 9  |-  ( Y  e.  V  ->  [_ Y  /  x ]_ B  =  a )
8332, 82syl 15 . . . . . . . 8  |-  ( ph  ->  [_ Y  /  x ]_ B  =  a
)
8483adantr 451 . . . . . . 7  |-  ( (
ph  /\  -.  ps )  ->  [_ Y  /  x ]_ B  =  a
)
8584eqcomd 2288 . . . . . 6  |-  ( (
ph  /\  -.  ps )  ->  a  =  [_ Y  /  x ]_ B )
8685a1d 22 . . . . 5  |-  ( (
ph  /\  -.  ps )  ->  ( -.  [. Y  /  x ]. ch  ->  a  =  [_ Y  /  x ]_ B ) )
8757, 61, 79, 86ifbothda 3595 . . . 4  |-  ( ph  ->  ( -.  [. if ( ps ,  X ,  Y )  /  x ]. ch  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
8849, 53, 87sylc 56 . . 3  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
89 csbeq1a 3089 . . . . 5  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  B  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B )
9089eqeq2d 2294 . . . 4  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  B  <->  a  =  [_ if ( ps ,  X ,  Y )  /  x ]_ B ) )
9190biimprd 214 . . 3  |-  ( x  =  if ( ps ,  X ,  Y
)  ->  ( a  =  [_ if ( ps ,  X ,  Y
)  /  x ]_ B  ->  a  =  B ) )
9248, 88, 91sylc 56 . 2  |-  ( ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
)  /\  -.  ch )  ->  a  =  B )
931, 2, 47, 92ifbothda 3595 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 176    /\ wa 358    = wceq 1623    e. wcel 1684   F/_wnfc 2406   [.wsbc 2991   [_csb 3081   ifcif 3565
This theorem is referenced by:  ballotlemsf1o  23072
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sbc 2992  df-csb 3082  df-if 3566
  Copyright terms: Public domain W3C validator