Step | Hyp | Ref
| Expression |
1 | | eqeq1 2736 |
. . . 4
โข (๐ = ๐ โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
2 | 1 | 2rexbidv 3219 |
. . 3
โข (๐ = ๐ โ (โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
3 | | oveq1 7401 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยทs ๐ต) = (๐ ยทs ๐ต)) |
4 | 3 | oveq1d 7409 |
. . . . . 6
โข (๐ = ๐ โ ((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) = ((๐ ยทs ๐ต) +s (๐ด ยทs ๐))) |
5 | | oveq1 7401 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยทs ๐) = (๐ ยทs ๐)) |
6 | 4, 5 | oveq12d 7412 |
. . . . 5
โข (๐ = ๐ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
7 | 6 | eqeq2d 2743 |
. . . 4
โข (๐ = ๐ โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
8 | | oveq2 7402 |
. . . . . . 7
โข (๐ = ๐ โ (๐ด ยทs ๐) = (๐ด ยทs ๐ )) |
9 | 8 | oveq2d 7410 |
. . . . . 6
โข (๐ = ๐ โ ((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) = ((๐ ยทs ๐ต) +s (๐ด ยทs ๐ ))) |
10 | | oveq2 7402 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยทs ๐) = (๐ ยทs ๐ )) |
11 | 9, 10 | oveq12d 7412 |
. . . . 5
โข (๐ = ๐ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) |
12 | 11 | eqeq2d 2743 |
. . . 4
โข (๐ = ๐ โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
13 | 7, 12 | cbvrex2vw 3239 |
. . 3
โข
(โ๐ โ
๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) |
14 | 2, 13 | bitrdi 286 |
. 2
โข (๐ = ๐ โ (โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
15 | 14 | cbvabv 2805 |
1
โข {๐ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} = {๐ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} |