Step |
Hyp |
Ref |
Expression |
1 |
|
indif1 |
⊢ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) = ( ( V ∩ dom 𝑅 ) ∖ { 𝑋 } ) |
2 |
|
incom |
⊢ ( V ∩ dom 𝑅 ) = ( dom 𝑅 ∩ V ) |
3 |
|
inv1 |
⊢ ( dom 𝑅 ∩ V ) = dom 𝑅 |
4 |
2 3
|
eqtri |
⊢ ( V ∩ dom 𝑅 ) = dom 𝑅 |
5 |
4
|
difeq1i |
⊢ ( ( V ∩ dom 𝑅 ) ∖ { 𝑋 } ) = ( dom 𝑅 ∖ { 𝑋 } ) |
6 |
1 5
|
eqtri |
⊢ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) = ( dom 𝑅 ∖ { 𝑋 } ) |
7 |
6
|
reseq2i |
⊢ ( 𝑅 ↾ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) ) = ( 𝑅 ↾ ( dom 𝑅 ∖ { 𝑋 } ) ) |
8 |
|
resindm |
⊢ ( Rel 𝑅 → ( 𝑅 ↾ ( ( V ∖ { 𝑋 } ) ∩ dom 𝑅 ) ) = ( 𝑅 ↾ ( V ∖ { 𝑋 } ) ) ) |
9 |
7 8
|
syl5reqr |
⊢ ( Rel 𝑅 → ( 𝑅 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝑅 ↾ ( dom 𝑅 ∖ { 𝑋 } ) ) ) |