ifeqeqx - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ifeqeqx		Structured version Visualization version GIF version

Theorem ifeqeqx 30291

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

**Hypotheses**
Ref	Expression
ifeqeqx.1	⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶)
ifeqeqx.2	⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎)
ifeqeqx.3	⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃))
ifeqeqx.4	⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓))
ifeqeqx.5	⊢ (𝜑 → 𝑎 = 𝐶)
ifeqeqx.6	⊢ ((𝜑 ∧ 𝜓) → 𝜃)
ifeqeqx.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
ifeqeqx.x	⊢ (𝜑 → 𝑋 ∈ 𝑊)

**Assertion**
Ref	Expression
ifeqeqx	⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))

Distinct variable groups: 𝑥,𝑎 𝑥,𝐶 𝑥,𝑋 𝑥,𝑌 𝑥,𝑉 𝑥,𝑊 𝜓,𝑥 𝜃,𝑥 Allowed substitution hints: 𝜑(𝑥,𝑎) 𝜓(𝑎) 𝜒(𝑥,𝑎) 𝜃(𝑎) 𝐴(𝑥,𝑎) 𝐵(𝑥,𝑎) 𝐶(𝑎) 𝑉(𝑎) 𝑊(𝑎) 𝑋(𝑎) 𝑌(𝑎)

**Proof of Theorem ifeqeqx**
Step	Hyp	Ref	Expression
1		eqeq2 2833	. 2 ⊢ (𝐴 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐴 ↔ 𝑎 = if(𝜒, 𝐴, 𝐵)))
2		eqeq2 2833	. 2 ⊢ (𝐵 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐵 ↔ 𝑎 = if(𝜒, 𝐴, 𝐵)))
3		simplr 767	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
4		simpll 765	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜑)
5		simpr 487	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜒)
6		sbceq1a 3782	. . . . . 6 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
7	6	biimpd 231	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒 → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
8	3, 5, 7	sylc 65	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
9		dfsbcq 3773	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ([𝑋 / 𝑥]𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
10		csbeq1 3885	. . . . . . 7 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ⦋𝑋 / 𝑥⦌𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
11	10	eqeq2d 2832	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑋 / 𝑥⦌𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
12	9, 11	imbi12d 347	. . . . 5 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (([𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)))
13		dfsbcq 3773	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ([𝑌 / 𝑥]𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
14		csbeq1 3885	. . . . . . 7 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ⦋𝑌 / 𝑥⦌𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
15	14	eqeq2d 2832	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑌 / 𝑥⦌𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
16	13, 15	imbi12d 347	. . . . 5 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (([𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)))
17		ifeqeqx.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝑊)
18		nfcvd 2978	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑊 → Ⅎ𝑥𝐶)
19		ifeqeqx.1	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶)
20	18, 19	csbiegf 3915	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌𝐴 = 𝐶)
21	17, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 = 𝐶)
22		ifeqeqx.5	. . . . . . . . 9 ⊢ (𝜑 → 𝑎 = 𝐶)
23	21, 22	eqtr4d 2859	. . . . . . . 8 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 = 𝑎)
24	23	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ⦋𝑋 / 𝑥⦌𝐴 = 𝑎)
25	24	eqcomd 2827	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴)
26	25	a1d 25	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ([𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴))
27		pm3.24 405	. . . . . . . . . 10 ⊢ ¬ (𝜓 ∧ ¬ 𝜓)
28		ifeqeqx.y	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
29		ifeqeqx.4	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓))
30	29	sbcieg 3809	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑥]𝜒 ↔ 𝜓))
31	28, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ([𝑌 / 𝑥]𝜒 ↔ 𝜓))
32	31	anbi1d 631	. . . . . . . . . 10 ⊢ (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) ↔ (𝜓 ∧ ¬ 𝜓)))
33	27, 32	mtbiri 329	. . . . . . . . 9 ⊢ (𝜑 → ¬ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓))
34	33	pm2.21d 121	. . . . . . . 8 ⊢ (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴))
35	34	imp 409	. . . . . . 7 ⊢ ((𝜑 ∧ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓)) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴)
36	35	anass1rs 653	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝜓) ∧ [𝑌 / 𝑥]𝜒) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴)
37	36	ex 415	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝜓) → ([𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴))
38	12, 16, 26, 37	ifbothda 4503	. . . 4 ⊢ (𝜑 → ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
39	4, 8, 38	sylc 65	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
40		csbeq1a 3896	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
41	40	eqeq2d 2832	. . . 4 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
42	41	biimprd 250	. . 3 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴 → 𝑎 = 𝐴))
43	3, 39, 42	sylc 65	. 2 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = 𝐴)
44		simplr 767	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
45		simpll 765	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝜑)
46		simpr 487	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ 𝜒)
47	6	notbid 320	. . . . . 6 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
48	47	biimpd 231	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
49	44, 46, 48	sylc 65	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
50	9	notbid 320	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
51		csbeq1 3885	. . . . . . 7 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ⦋𝑋 / 𝑥⦌𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
52	51	eqeq2d 2832	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
53	50, 52	imbi12d 347	. . . . 5 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)))
54	13	notbid 320	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑌 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
55		csbeq1 3885	. . . . . . 7 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ⦋𝑌 / 𝑥⦌𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
56	55	eqeq2d 2832	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑌 / 𝑥⦌𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
57	54, 56	imbi12d 347	. . . . 5 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)))
58		ifeqeqx.3	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃))
59	58	sbcieg 3809	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑊 → ([𝑋 / 𝑥]𝜒 ↔ 𝜃))
60	17, 59	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ([𝑋 / 𝑥]𝜒 ↔ 𝜃))
61	60	notbid 320	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ 𝜃))
62	61	biimpd 231	. . . . . . . . . 10 ⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜃))
63		ifeqeqx.6	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
64	63	ex 415	. . . . . . . . . 10 ⊢ (𝜑 → (𝜓 → 𝜃))
65	62, 64	nsyld 159	. . . . . . . . 9 ⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜓))
66	65	anim2d 613	. . . . . . . 8 ⊢ (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → (𝜓 ∧ ¬ 𝜓)))
67	27, 66	mtoi 201	. . . . . . 7 ⊢ (𝜑 → ¬ (𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒))
68	67	pm2.21d 121	. . . . . 6 ⊢ (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵))
69	68	expdimp 455	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (¬ [𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵))
70		nfcvd 2978	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝑉 → Ⅎ𝑥𝑎)
71		ifeqeqx.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎)
72	70, 71	csbiegf 3915	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑉 → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎)
73	28, 72	syl 17	. . . . . . . 8 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎)
74	73	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝜓) → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎)
75	74	eqcomd 2827	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵)
76	75	a1d 25	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝜓) → (¬ [𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵))
77	53, 57, 69, 76	ifbothda 4503	. . . 4 ⊢ (𝜑 → (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
78	45, 49, 77	sylc 65	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
79		csbeq1a 3896	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
80	79	eqeq2d 2832	. . . 4 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
81	80	biimprd 250	. . 3 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵 → 𝑎 = 𝐵))
82	44, 78, 81	sylc 65	. 2 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = 𝐵)
83	1, 2, 43, 82	ifbothda 4503	1 ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 [wsbc 3771 ⦋csb 3882 ifcif 4466

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-sbc 3772 df-csb 3883 df-if 4467

This theorem is referenced by: ballotlemsf1o 31766

W3C validator