Theorem ifeqeqx

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

	Ref	Expression
Hypotheses	ifeqeqx.1	$$⊢x=X\to A=C$$
	ifeqeqx.2	$$⊢x=Y\to B=a$$
	ifeqeqx.3	$$⊢x=X\to \left(\chi \leftrightarrow \theta \right)$$
	ifeqeqx.4	$$⊢x=Y\to \left(\chi \leftrightarrow \psi \right)$$
	ifeqeqx.5	$$⊢\phi \to a=C$$
	ifeqeqx.6	$$⊢\left(\phi \wedge \psi \right)\to \theta$$
	ifeqeqx.y	$$⊢\phi \to Y\in V$$
	ifeqeqx.x	$$⊢\phi \to X\in W$$
Assertion	ifeqeqx	$$⊢\left(\phi \wedge x=if\left(\psi ,X,Y\right)\right)\to a=if\left(\chi ,A,B\right)$$

Proof

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