Theorem ifeqeqx 29361

Description: An equality theorem tailored for ballotlemsf1o 30575. (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

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   [.wsbc 3435   [_csb 3533   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sbc 3436  df-csb 3534  df-if 4087

This theorem is referenced by:  ballotlemsf1o  30575