Theorem ifeqeqxdc 3673

Description: An equality theorem tailored for ballotfilemsf1o 13201. (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 )
ifeqeqxdc.dc	|- ( ph -> DECID ps )

Assertion

Ref	Expression
ifeqeqxdc	|- ( ( 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 ifeqeqxdc

Step	Hyp	Ref	Expression
1		eqeq2 2244	. 2 |- ( A = if ( ch , A , B ) -> ( a = A <-> a = if ( ch , A , B ) ) )
2		eqeq2 2244	. 2 |- ( B = if ( ch , A , B ) -> ( a = B <-> a = if ( ch , A , B ) ) )
3		simplr 529	. . 3 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> x = if ( ps , X , Y ) )
4		simpll 527	. . . 4 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> ph )
5		simpr 110	. . . . 5 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> ch )
6		sbceq1a 3055	. . . . . 6 |- ( x = if ( ps , X , Y ) -> ( ch <-> [. if ( ps , X , Y ) / x ]. ch ) )
7	6	biimpd 144	. . . . 5 |- ( x = if ( ps , X , Y ) -> ( ch -> [. if ( ps , X , Y ) / x ]. ch ) )
8	3, 5, 7	sylc 62	. . . 4 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> [. if ( ps , X , Y ) / x ]. ch )
9		dfsbcq 3047	. . . . . 6 |- ( X = if ( ps , X , Y ) -> ( [. X / x ]. ch <-> [. if ( ps , X , Y ) / x ]. ch ) )
10		csbeq1 3144	. . . . . . 7 |- ( X = if ( ps , X , Y ) -> [_ X / x ]_ A = [_ if ( ps , X , Y ) / x ]_ A )
11	10	eqeq2d 2246	. . . . . 6 |- ( X = if ( ps , X , Y ) -> ( a = [_ X / x ]_ A <-> a = [_ if ( ps , X , Y ) / x ]_ A ) )
12	9, 11	imbi12d 234	. . . . 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 3047	. . . . . 6 |- ( Y = if ( ps , X , Y ) -> ( [. Y / x ]. ch <-> [. if ( ps , X , Y ) / x ]. ch ) )
14		csbeq1 3144	. . . . . . 7 |- ( Y = if ( ps , X , Y ) -> [_ Y / x ]_ A = [_ if ( ps , X , Y ) / x ]_ A )
15	14	eqeq2d 2246	. . . . . 6 |- ( Y = if ( ps , X , Y ) -> ( a = [_ Y / x ]_ A <-> a = [_ if ( ps , X , Y ) / x ]_ A ) )
16	13, 15	imbi12d 234	. . . . 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 2387	. . . . . . . . . . 11 |- ( X e. W -> F/_ x C )
19		ifeqeqx.1	. . . . . . . . . . 11 |- ( x = X -> A = C )
20	18, 19	csbiegf 3185	. . . . . . . . . 10 |- ( X e. W -> [_ X / x ]_ A = C )
21	17, 20	syl 14	. . . . . . . . 9 |- ( ph -> [_ X / x ]_ A = C )
22		ifeqeqx.5	. . . . . . . . 9 |- ( ph -> a = C )
23	21, 22	eqtr4d 2270	. . . . . . . 8 |- ( ph -> [_ X / x ]_ A = a )
24	23	adantr 276	. . . . . . 7 |- ( ( ph /\ ps ) -> [_ X / x ]_ A = a )
25	24	eqcomd 2240	. . . . . 6 |- ( ( ph /\ ps ) -> a = [_ X / x ]_ A )
26	25	a1d 22	. . . . 5 |- ( ( ph /\ ps ) -> ( [. X / x ]. ch -> a = [_ X / x ]_ A ) )
27		pm3.24 701	. . . . . . . . . 10 |- -. ( ps /\ -. ps )
28		ifeqeqx.y	. . . . . . . . . . . 12 |- ( ph -> Y e. V )
29		ifeqeqx.4	. . . . . . . . . . . . 13 |- ( x = Y -> ( ch <-> ps ) )
30	29	sbcieg 3078	. . . . . . . . . . . 12 |- ( Y e. V -> ( [. Y / x ]. ch <-> ps ) )
31	28, 30	syl 14	. . . . . . . . . . 11 |- ( ph -> ( [. Y / x ]. ch <-> ps ) )
32	31	anbi1d 465	. . . . . . . . . 10 |- ( ph -> ( ( [. Y / x ]. ch /\ -. ps ) <-> ( ps /\ -. ps ) ) )
33	27, 32	mtbiri 682	. . . . . . . . 9 |- ( ph -> -. ( [. Y / x ]. ch /\ -. ps ) )
34	33	pm2.21d 624	. . . . . . . 8 |- ( ph -> ( ( [. Y / x ]. ch /\ -. ps ) -> a = [_ Y / x ]_ A ) )
35	34	imp 124	. . . . . . 7 |- ( ( ph /\ ( [. Y / x ]. ch /\ -. ps ) ) -> a = [_ Y / x ]_ A )
36	35	anass1rs 573	. . . . . 6 |- ( ( ( ph /\ -. ps ) /\ [. Y / x ]. ch ) -> a = [_ Y / x ]_ A )
37	36	ex 115	. . . . 5 |- ( ( ph /\ -. ps ) -> ( [. Y / x ]. ch -> a = [_ Y / x ]_ A ) )
38		ifeqeqxdc.dc	. . . . 5 |- ( ph -> DECID ps )
39	12, 16, 26, 37, 38	ifbothdadc 3660	. . . 4 |- ( ph -> ( [. if ( ps , X , Y ) / x ]. ch -> a = [_ if ( ps , X , Y ) / x ]_ A ) )
40	4, 8, 39	sylc 62	. . 3 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> a = [_ if ( ps , X , Y ) / x ]_ A )
41		csbeq1a 3150	. . . . 5 |- ( x = if ( ps , X , Y ) -> A = [_ if ( ps , X , Y ) / x ]_ A )
42	41	eqeq2d 2246	. . . 4 |- ( x = if ( ps , X , Y ) -> ( a = A <-> a = [_ if ( ps , X , Y ) / x ]_ A ) )
43	42	biimprd 158	. . 3 |- ( x = if ( ps , X , Y ) -> ( a = [_ if ( ps , X , Y ) / x ]_ A -> a = A ) )
44	3, 40, 43	sylc 62	. 2 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ch ) -> a = A )
45		simplr 529	. . 3 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> x = if ( ps , X , Y ) )
46		simpll 527	. . . 4 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> ph )
47		simpr 110	. . . . 5 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> -. ch )
48	6	notbid 673	. . . . . 6 |- ( x = if ( ps , X , Y ) -> ( -. ch <-> -. [. if ( ps , X , Y ) / x ]. ch ) )
49	48	biimpd 144	. . . . 5 |- ( x = if ( ps , X , Y ) -> ( -. ch -> -. [. if ( ps , X , Y ) / x ]. ch ) )
50	45, 47, 49	sylc 62	. . . 4 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> -. [. if ( ps , X , Y ) / x ]. ch )
51	9	notbid 673	. . . . . 6 |- ( X = if ( ps , X , Y ) -> ( -. [. X / x ]. ch <-> -. [. if ( ps , X , Y ) / x ]. ch ) )
52		csbeq1 3144	. . . . . . 7 |- ( X = if ( ps , X , Y ) -> [_ X / x ]_ B = [_ if ( ps , X , Y ) / x ]_ B )
53	52	eqeq2d 2246	. . . . . 6 |- ( X = if ( ps , X , Y ) -> ( a = [_ X / x ]_ B <-> a = [_ if ( ps , X , Y ) / x ]_ B ) )
54	51, 53	imbi12d 234	. . . . 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 ) ) )
55	13	notbid 673	. . . . . 6 |- ( Y = if ( ps , X , Y ) -> ( -. [. Y / x ]. ch <-> -. [. if ( ps , X , Y ) / x ]. ch ) )
56		csbeq1 3144	. . . . . . 7 |- ( Y = if ( ps , X , Y ) -> [_ Y / x ]_ B = [_ if ( ps , X , Y ) / x ]_ B )
57	56	eqeq2d 2246	. . . . . 6 |- ( Y = if ( ps , X , Y ) -> ( a = [_ Y / x ]_ B <-> a = [_ if ( ps , X , Y ) / x ]_ B ) )
58	55, 57	imbi12d 234	. . . . 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 ) ) )
59		ifeqeqx.3	. . . . . . . . . . . . . 14 |- ( x = X -> ( ch <-> th ) )
60	59	sbcieg 3078	. . . . . . . . . . . . 13 |- ( X e. W -> ( [. X / x ]. ch <-> th ) )
61	17, 60	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( [. X / x ]. ch <-> th ) )
62	61	notbid 673	. . . . . . . . . . 11 |- ( ph -> ( -. [. X / x ]. ch <-> -. th ) )
63	62	biimpd 144	. . . . . . . . . 10 |- ( ph -> ( -. [. X / x ]. ch -> -. th ) )
64		ifeqeqx.6	. . . . . . . . . . 11 |- ( ( ph /\ ps ) -> th )
65	64	ex 115	. . . . . . . . . 10 |- ( ph -> ( ps -> th ) )
66	63, 65	nsyld 653	. . . . . . . . 9 |- ( ph -> ( -. [. X / x ]. ch -> -. ps ) )
67	66	anim2d 337	. . . . . . . 8 |- ( ph -> ( ( ps /\ -. [. X / x ]. ch ) -> ( ps /\ -. ps ) ) )
68	27, 67	mtoi 670	. . . . . . 7 |- ( ph -> -. ( ps /\ -. [. X / x ]. ch ) )
69	68	pm2.21d 624	. . . . . 6 |- ( ph -> ( ( ps /\ -. [. X / x ]. ch ) -> a = [_ X / x ]_ B ) )
70	69	expdimp 259	. . . . 5 |- ( ( ph /\ ps ) -> ( -. [. X / x ]. ch -> a = [_ X / x ]_ B ) )
71		nfcvd 2387	. . . . . . . . . 10 |- ( Y e. V -> F/_ x a )
72		ifeqeqx.2	. . . . . . . . . 10 |- ( x = Y -> B = a )
73	71, 72	csbiegf 3185	. . . . . . . . 9 |- ( Y e. V -> [_ Y / x ]_ B = a )
74	28, 73	syl 14	. . . . . . . 8 |- ( ph -> [_ Y / x ]_ B = a )
75	74	adantr 276	. . . . . . 7 |- ( ( ph /\ -. ps ) -> [_ Y / x ]_ B = a )
76	75	eqcomd 2240	. . . . . 6 |- ( ( ph /\ -. ps ) -> a = [_ Y / x ]_ B )
77	76	a1d 22	. . . . 5 |- ( ( ph /\ -. ps ) -> ( -. [. Y / x ]. ch -> a = [_ Y / x ]_ B ) )
78	54, 58, 70, 77, 38	ifbothdadc 3660	. . . 4 |- ( ph -> ( -. [. if ( ps , X , Y ) / x ]. ch -> a = [_ if ( ps , X , Y ) / x ]_ B ) )
79	46, 50, 78	sylc 62	. . 3 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> a = [_ if ( ps , X , Y ) / x ]_ B )
80		csbeq1a 3150	. . . . 5 |- ( x = if ( ps , X , Y ) -> B = [_ if ( ps , X , Y ) / x ]_ B )
81	80	eqeq2d 2246	. . . 4 |- ( x = if ( ps , X , Y ) -> ( a = B <-> a = [_ if ( ps , X , Y ) / x ]_ B ) )
82	81	biimprd 158	. . 3 |- ( x = if ( ps , X , Y ) -> ( a = [_ if ( ps , X , Y ) / x ]_ B -> a = B ) )
83	45, 79, 82	sylc 62	. 2 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ch ) -> a = B )
84	64	adantlr 477	. . . . . 6 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> th )
85		simplr 529	. . . . . . . 8 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> x = if ( ps , X , Y ) )
86		simpr 110	. . . . . . . . 9 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> ps )
87	86	iftrued 3633	. . . . . . . 8 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> if ( ps , X , Y ) = X )
88	85, 87	eqtrd 2267	. . . . . . 7 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> x = X )
89	88, 59	syl 14	. . . . . 6 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> ( ch <-> th ) )
90	84, 89	mpbird 167	. . . . 5 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> ch )
91	90	orcd 741	. . . 4 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> ( ch \/ -. ch ) )
92		df-dc 843	. . . 4 |- (DECID ch <-> ( ch \/ -. ch ) )
93	91, 92	sylibr 134	. . 3 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ ps ) -> DECID ch )
94	38	ad2antrr 488	. . . 4 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> DECID ps )
95		simplr 529	. . . . . . 7 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> x = if ( ps , X , Y ) )
96		simpr 110	. . . . . . . 8 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> -. ps )
97	96	iffalsed 3636	. . . . . . 7 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> if ( ps , X , Y ) = Y )
98	95, 97	eqtrd 2267	. . . . . 6 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> x = Y )
99	98, 29	syl 14	. . . . 5 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> ( ch <-> ps ) )
100	99	dcbid 846	. . . 4 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> (DECID ch <-> DECID ps ) )
101	94, 100	mpbird 167	. . 3 |- ( ( ( ph /\ x = if ( ps , X , Y ) ) /\ -. ps ) -> DECID ch )
102		exmiddc 844	. . . . 5 |- (DECID ps -> ( ps \/ -. ps ) )
103	38, 102	syl 14	. . . 4 |- ( ph -> ( ps \/ -. ps ) )
104	103	adantr 276	. . 3 |- ( ( ph /\ x = if ( ps , X , Y ) ) -> ( ps \/ -. ps ) )
105	93, 101, 104	mpjaodan 806	. 2 |- ( ( ph /\ x = if ( ps , X , Y ) ) -> DECID ch )
106	1, 2, 44, 83, 105	ifbothdadc 3660	1 |- ( ( ph /\ x = if ( ps , X , Y ) ) -> a = if ( ch , A , B ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 716  DECID wdc 842   = wceq 1398   e. wcel 2205   [.wsbc 3045   [_csb 3141   ifcif 3624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-sbc 3046  df-csb 3142  df-if 3625

This theorem is referenced by:  ballotfilemsf1o  13201