Proof of Theorem ifeqeqx
Step | Hyp | Ref
| Expression |
1 | | eqeq2 2749 |
. 2
⊢ (𝐴 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐴 ↔ 𝑎 = if(𝜒, 𝐴, 𝐵))) |
2 | | eqeq2 2749 |
. 2
⊢ (𝐵 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐵 ↔ 𝑎 = if(𝜒, 𝐴, 𝐵))) |
3 | | simplr 769 |
. . 3
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌)) |
4 | | simpll 767 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜑) |
5 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜒) |
6 | | sbceq1a 3705 |
. . . . . 6
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
7 | 6 | biimpd 232 |
. . . . 5
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒 → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
8 | 3, 5, 7 | sylc 65 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒) |
9 | | dfsbcq 3696 |
. . . . . 6
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ([𝑋 / 𝑥]𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
10 | | csbeq1 3814 |
. . . . . . 7
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ⦋𝑋 / 𝑥⦌𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴) |
11 | 10 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑋 / 𝑥⦌𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)) |
12 | 9, 11 | imbi12d 348 |
. . . . 5
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (([𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))) |
13 | | dfsbcq 3696 |
. . . . . 6
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ([𝑌 / 𝑥]𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
14 | | csbeq1 3814 |
. . . . . . 7
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ⦋𝑌 / 𝑥⦌𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴) |
15 | 14 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑌 / 𝑥⦌𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)) |
16 | 13, 15 | imbi12d 348 |
. . . . 5
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (([𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))) |
17 | | ifeqeqx.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
18 | | nfcvd 2905 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑊 → Ⅎ𝑥𝐶) |
19 | | ifeqeqx.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶) |
20 | 18, 19 | csbiegf 3845 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌𝐴 = 𝐶) |
21 | 17, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 = 𝐶) |
22 | | ifeqeqx.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝑎 = 𝐶) |
23 | 21, 22 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 = 𝑎) |
24 | 23 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ⦋𝑋 / 𝑥⦌𝐴 = 𝑎) |
25 | 24 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴) |
26 | 25 | a1d 25 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ([𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴)) |
27 | | pm3.24 406 |
. . . . . . . . . 10
⊢ ¬
(𝜓 ∧ ¬ 𝜓) |
28 | | ifeqeqx.y |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
29 | | ifeqeqx.4 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓)) |
30 | 29 | sbcieg 3734 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑥]𝜒 ↔ 𝜓)) |
31 | 28, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ([𝑌 / 𝑥]𝜒 ↔ 𝜓)) |
32 | 31 | anbi1d 633 |
. . . . . . . . . 10
⊢ (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) ↔ (𝜓 ∧ ¬ 𝜓))) |
33 | 27, 32 | mtbiri 330 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓)) |
34 | 33 | pm2.21d 121 |
. . . . . . . 8
⊢ (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴)) |
35 | 34 | imp 410 |
. . . . . . 7
⊢ ((𝜑 ∧ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓)) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴) |
36 | 35 | anass1rs 655 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝜓) ∧ [𝑌 / 𝑥]𝜒) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴) |
37 | 36 | ex 416 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝜓) → ([𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴)) |
38 | 12, 16, 26, 37 | ifbothda 4477 |
. . . 4
⊢ (𝜑 → ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)) |
39 | 4, 8, 38 | sylc 65 |
. . 3
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴) |
40 | | csbeq1a 3825 |
. . . . 5
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴) |
41 | 40 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)) |
42 | 41 | biimprd 251 |
. . 3
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴 → 𝑎 = 𝐴)) |
43 | 3, 39, 42 | sylc 65 |
. 2
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = 𝐴) |
44 | | simplr 769 |
. . 3
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌)) |
45 | | simpll 767 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝜑) |
46 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ 𝜒) |
47 | 6 | notbid 321 |
. . . . . 6
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
48 | 47 | biimpd 232 |
. . . . 5
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
49 | 44, 46, 48 | sylc 65 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒) |
50 | 9 | notbid 321 |
. . . . . 6
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
51 | | csbeq1 3814 |
. . . . . . 7
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ⦋𝑋 / 𝑥⦌𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵) |
52 | 51 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)) |
53 | 50, 52 | imbi12d 348 |
. . . . 5
⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))) |
54 | 13 | notbid 321 |
. . . . . 6
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑌 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)) |
55 | | csbeq1 3814 |
. . . . . . 7
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ⦋𝑌 / 𝑥⦌𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵) |
56 | 55 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑌 / 𝑥⦌𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)) |
57 | 54, 56 | imbi12d 348 |
. . . . 5
⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))) |
58 | | ifeqeqx.3 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃)) |
59 | 58 | sbcieg 3734 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑊 → ([𝑋 / 𝑥]𝜒 ↔ 𝜃)) |
60 | 17, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ([𝑋 / 𝑥]𝜒 ↔ 𝜃)) |
61 | 60 | notbid 321 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ 𝜃)) |
62 | 61 | biimpd 232 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜃)) |
63 | | ifeqeqx.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
64 | 63 | ex 416 |
. . . . . . . . . 10
⊢ (𝜑 → (𝜓 → 𝜃)) |
65 | 62, 64 | nsyld 159 |
. . . . . . . . 9
⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜓)) |
66 | 65 | anim2d 615 |
. . . . . . . 8
⊢ (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → (𝜓 ∧ ¬ 𝜓))) |
67 | 27, 66 | mtoi 202 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒)) |
68 | 67 | pm2.21d 121 |
. . . . . 6
⊢ (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵)) |
69 | 68 | expdimp 456 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (¬ [𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵)) |
70 | | nfcvd 2905 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝑉 → Ⅎ𝑥𝑎) |
71 | | ifeqeqx.2 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎) |
72 | 70, 71 | csbiegf 3845 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝑉 → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎) |
73 | 28, 72 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎) |
74 | 73 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝜓) → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎) |
75 | 74 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵) |
76 | 75 | a1d 25 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝜓) → (¬ [𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵)) |
77 | 53, 57, 69, 76 | ifbothda 4477 |
. . . 4
⊢ (𝜑 → (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)) |
78 | 45, 49, 77 | sylc 65 |
. . 3
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵) |
79 | | csbeq1a 3825 |
. . . . 5
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵) |
80 | 79 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)) |
81 | 80 | biimprd 251 |
. . 3
⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵 → 𝑎 = 𝐵)) |
82 | 44, 78, 81 | sylc 65 |
. 2
⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = 𝐵) |
83 | 1, 2, 43, 82 | ifbothda 4477 |
1
⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵)) |