Step |
Hyp |
Ref |
Expression |
1 |
|
resundi |
⊢ ( 𝐴 ↾ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ↾ 𝐵 ) ∪ ( 𝐴 ↾ 𝐶 ) ) |
2 |
1
|
rneqi |
⊢ ran ( 𝐴 ↾ ( 𝐵 ∪ 𝐶 ) ) = ran ( ( 𝐴 ↾ 𝐵 ) ∪ ( 𝐴 ↾ 𝐶 ) ) |
3 |
|
rnun |
⊢ ran ( ( 𝐴 ↾ 𝐵 ) ∪ ( 𝐴 ↾ 𝐶 ) ) = ( ran ( 𝐴 ↾ 𝐵 ) ∪ ran ( 𝐴 ↾ 𝐶 ) ) |
4 |
2 3
|
eqtri |
⊢ ran ( 𝐴 ↾ ( 𝐵 ∪ 𝐶 ) ) = ( ran ( 𝐴 ↾ 𝐵 ) ∪ ran ( 𝐴 ↾ 𝐶 ) ) |
5 |
|
df-ima |
⊢ ( 𝐴 “ ( 𝐵 ∪ 𝐶 ) ) = ran ( 𝐴 ↾ ( 𝐵 ∪ 𝐶 ) ) |
6 |
|
df-ima |
⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 ) |
7 |
|
df-ima |
⊢ ( 𝐴 “ 𝐶 ) = ran ( 𝐴 ↾ 𝐶 ) |
8 |
6 7
|
uneq12i |
⊢ ( ( 𝐴 “ 𝐵 ) ∪ ( 𝐴 “ 𝐶 ) ) = ( ran ( 𝐴 ↾ 𝐵 ) ∪ ran ( 𝐴 ↾ 𝐶 ) ) |
9 |
4 5 8
|
3eqtr4i |
⊢ ( 𝐴 “ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 “ 𝐵 ) ∪ ( 𝐴 “ 𝐶 ) ) |