Metamath Proof Explorer

Theorem ifeqeqx

Description: An equality theorem tailored for ballotlemsf1o . (Contributed by Thierry Arnoux, 14-Apr-2017)

Ref Expression
Hypotheses 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 ifeqeqx 
|- ( ( ph /\ x = if ( ps , X , Y ) ) -> a = if ( ch , A , B ) )

Proof

Step Hyp Ref Expression
1 ifeqeqx.1 
 |-  ( x = X -> A = C )
2 ifeqeqx.2 
 |-  ( x = Y -> B = a )
3 ifeqeqx.3 
 |-  ( x = X -> ( ch <-> th ) )
4 ifeqeqx.4 
 |-  ( x = Y -> ( ch <-> ps ) )
5 ifeqeqx.5 
 |-  ( ph -> a = C )
6 ifeqeqx.6 
 |-  ( ( ph /\ ps ) -> th )
7 ifeqeqx.y 
 |-  ( ph -> Y e. V )
8 ifeqeqx.x 
 |-  ( ph -> X e. W )
9 eqeq2 
 |-  ( A = if ( ch , A , B ) -> ( a = A <-> a = if ( ch , A , B ) ) )
10 eqeq2 
 |-  ( B = if ( ch , A , B ) -> ( a = B <-> a = if ( ch , A , B ) ) )
11 simplr 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> x = if ( ps , X , Y ) )
12 simpll 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> ph )
13 simpr 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> ch )
14 sbceq1a 
 |-  ( x = if ( ps , X , Y ) -> ( ch <-> [. if ( ps , X , Y ) / x ]. ch ) )
15 14 biimpd 
 |-  ( x = if ( ps , X , Y ) -> ( ch -> [. if ( ps , X , Y ) / x ]. ch ) )
16 11 13 15 sylc 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> [. if ( ps , X , Y ) / x ]. ch )
17 dfsbcq 
 |-  ( X = if ( ps , X , Y ) -> ( [. X / x ]. ch <-> [. if ( ps , X , Y ) / x ]. ch ) )
18 csbeq1 
 |-  ( X = if ( ps , X , Y ) -> [_ X / x ]_ A = [_ if ( ps , X , Y ) / x ]_ A )
19 18 eqeq2d 
 |-  ( X = if ( ps , X , Y ) -> ( a = [_ X / x ]_ A <-> a = [_ if ( ps , X , Y ) / x ]_ A ) )
20 17 19 imbi12d 
 |-  ( 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 ) ) )
21 dfsbcq 
 |-  ( Y = if ( ps , X , Y ) -> ( [. Y / x ]. ch <-> [. if ( ps , X , Y ) / x ]. ch ) )
22 csbeq1 
 |-  ( Y = if ( ps , X , Y ) -> [_ Y / x ]_ A = [_ if ( ps , X , Y ) / x ]_ A )
23 22 eqeq2d 
 |-  ( Y = if ( ps , X , Y ) -> ( a = [_ Y / x ]_ A <-> a = [_ if ( ps , X , Y ) / x ]_ A ) )
24 21 23 imbi12d 
 |-  ( 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 ) ) )
25 nfcvd 
 |-  ( X e. W -> F/_ x C )
26 25 1 csbiegf 
 |-  ( X e. W -> [_ X / x ]_ A = C )
27 8 26 syl 
 |-  ( ph -> [_ X / x ]_ A = C )
28 27 5 eqtr4d 
 |-  ( ph -> [_ X / x ]_ A = a )
29 28 adantr 
 |-  ( ( ph /\ ps ) -> [_ X / x ]_ A = a )
30 29 eqcomd 
 |-  ( ( ph /\ ps ) -> a = [_ X / x ]_ A )
31 30 a1d 
 |-  ( ( ph /\ ps ) -> ( [. X / x ]. ch -> a = [_ X / x ]_ A ) )
32 pm3.24 
 |-  -. ( ps /\ -. ps )
33 4 sbcieg 
 |-  ( Y e. V -> ( [. Y / x ]. ch <-> ps ) )
34 7 33 syl 
 |-  ( ph -> ( [. Y / x ]. ch <-> ps ) )
35 34 anbi1d 
 |-  ( ph -> ( ( [. Y / x ]. ch /\ -. ps ) <-> ( ps /\ -. ps ) ) )
36 32 35 mtbiri 
 |-  ( ph -> -. ( [. Y / x ]. ch /\ -. ps ) )
37 36 pm2.21d 
 |-  ( ph -> ( ( [. Y / x ]. ch /\ -. ps ) -> a = [_ Y / x ]_ A ) )
38 37 imp 
 |-  ( ( ph /\ ( [. Y / x ]. ch /\ -. ps ) ) -> a = [_ Y / x ]_ A )
39 38 anass1rs 
 |-  ( ( ( ph /\ -. ps ) /\ [. Y / x ]. ch ) -> a = [_ Y / x ]_ A )
40 39 ex 
 |-  ( ( ph /\ -. ps ) -> ( [. Y / x ]. ch -> a = [_ Y / x ]_ A ) )
41 20 24 31 40 ifbothda 
 |-  ( ph -> ( [. if ( ps , X , Y ) / x ]. ch -> a = [_ if ( ps , X , Y ) / x ]_ A ) )
42 12 16 41 sylc 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> a = [_ if ( ps , X , Y ) / x ]_ A )
43 csbeq1a 
 |-  ( x = if ( ps , X , Y ) -> A = [_ if ( ps , X , Y ) / x ]_ A )
44 43 eqeq2d 
 |-  ( x = if ( ps , X , Y ) -> ( a = A <-> a = [_ if ( ps , X , Y ) / x ]_ A ) )
45 44 biimprd 
 |-  ( x = if ( ps , X , Y ) -> ( a = [_ if ( ps , X , Y ) / x ]_ A -> a = A ) )
46 11 42 45 sylc 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> a = A )
47 simplr 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> x = if ( ps , X , Y ) )
48 simpll 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> ph )
49 simpr 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> -. ch )
50 14 notbid 
 |-  ( x = if ( ps , X , Y ) -> ( -. ch <-> -. [. if ( ps , X , Y ) / x ]. ch ) )
51 50 biimpd 
 |-  ( x = if ( ps , X , Y ) -> ( -. ch -> -. [. if ( ps , X , Y ) / x ]. ch ) )
52 47 49 51 sylc 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> -. [. if ( ps , X , Y ) / x ]. ch )
53 17 notbid 
 |-  ( X = if ( ps , X , Y ) -> ( -. [. X / x ]. ch <-> -. [. if ( ps , X , Y ) / x ]. ch ) )
54 csbeq1 
 |-  ( X = if ( ps , X , Y ) -> [_ X / x ]_ B = [_ if ( ps , X , Y ) / x ]_ B )
55 54 eqeq2d 
 |-  ( X = if ( ps , X , Y ) -> ( a = [_ X / x ]_ B <-> a = [_ if ( ps , X , Y ) / x ]_ B ) )
56 53 55 imbi12d 
 |-  ( 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 ) ) )
57 21 notbid 
 |-  ( Y = if ( ps , X , Y ) -> ( -. [. Y / x ]. ch <-> -. [. if ( ps , X , Y ) / x ]. ch ) )
58 csbeq1 
 |-  ( Y = if ( ps , X , Y ) -> [_ Y / x ]_ B = [_ if ( ps , X , Y ) / x ]_ B )
59 58 eqeq2d 
 |-  ( Y = if ( ps , X , Y ) -> ( a = [_ Y / x ]_ B <-> a = [_ if ( ps , X , Y ) / x ]_ B ) )
60 57 59 imbi12d 
 |-  ( 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 ) ) )
61 3 sbcieg 
 |-  ( X e. W -> ( [. X / x ]. ch <-> th ) )
62 8 61 syl 
 |-  ( ph -> ( [. X / x ]. ch <-> th ) )
63 62 notbid 
 |-  ( ph -> ( -. [. X / x ]. ch <-> -. th ) )
64 63 biimpd 
 |-  ( ph -> ( -. [. X / x ]. ch -> -. th ) )
65 6 ex 
 |-  ( ph -> ( ps -> th ) )
66 64 65 nsyld 
 |-  ( ph -> ( -. [. X / x ]. ch -> -. ps ) )
67 66 anim2d 
 |-  ( ph -> ( ( ps /\ -. [. X / x ]. ch ) -> ( ps /\ -. ps ) ) )
68 32 67 mtoi 
 |-  ( ph -> -. ( ps /\ -. [. X / x ]. ch ) )
69 68 pm2.21d 
 |-  ( ph -> ( ( ps /\ -. [. X / x ]. ch ) -> a = [_ X / x ]_ B ) )
70 69 expdimp 
 |-  ( ( ph /\ ps ) -> ( -. [. X / x ]. ch -> a = [_ X / x ]_ B ) )
71 nfcvd 
 |-  ( Y e. V -> F/_ x a )
72 71 2 csbiegf 
 |-  ( Y e. V -> [_ Y / x ]_ B = a )
73 7 72 syl 
 |-  ( ph -> [_ Y / x ]_ B = a )
74 73 adantr 
 |-  ( ( ph /\ -. ps ) -> [_ Y / x ]_ B = a )
75 74 eqcomd 
 |-  ( ( ph /\ -. ps ) -> a = [_ Y / x ]_ B )
76 75 a1d 
 |-  ( ( ph /\ -. ps ) -> ( -. [. Y / x ]. ch -> a = [_ Y / x ]_ B ) )
77 56 60 70 76 ifbothda 
 |-  ( ph -> ( -. [. if ( ps , X , Y ) / x ]. ch -> a = [_ if ( ps , X , Y ) / x ]_ B ) )
78 48 52 77 sylc 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> a = [_ if ( ps , X , Y ) / x ]_ B )
79 csbeq1a 
 |-  ( x = if ( ps , X , Y ) -> B = [_ if ( ps , X , Y ) / x ]_ B )
80 79 eqeq2d 
 |-  ( x = if ( ps , X , Y ) -> ( a = B <-> a = [_ if ( ps , X , Y ) / x ]_ B ) )
81 80 biimprd 
 |-  ( x = if ( ps , X , Y ) -> ( a = [_ if ( ps , X , Y ) / x ]_ B -> a = B ) )
82 47 78 81 sylc 
 |-  ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> a = B )
83 9 10 46 82 ifbothda 
 |-  ( ( ph /\ x = if ( ps , X , Y ) ) -> a = if ( ch , A , B ) )