Step |
Hyp |
Ref |
Expression |
1 |
|
indif1 |
|- ( ( _V \ { X } ) i^i dom R ) = ( ( _V i^i dom R ) \ { X } ) |
2 |
|
incom |
|- ( _V i^i dom R ) = ( dom R i^i _V ) |
3 |
|
inv1 |
|- ( dom R i^i _V ) = dom R |
4 |
2 3
|
eqtri |
|- ( _V i^i dom R ) = dom R |
5 |
4
|
difeq1i |
|- ( ( _V i^i dom R ) \ { X } ) = ( dom R \ { X } ) |
6 |
1 5
|
eqtri |
|- ( ( _V \ { X } ) i^i dom R ) = ( dom R \ { X } ) |
7 |
6
|
reseq2i |
|- ( R |` ( ( _V \ { X } ) i^i dom R ) ) = ( R |` ( dom R \ { X } ) ) |
8 |
|
resindm |
|- ( Rel R -> ( R |` ( ( _V \ { X } ) i^i dom R ) ) = ( R |` ( _V \ { X } ) ) ) |
9 |
7 8
|
syl5reqr |
|- ( Rel R -> ( R |` ( _V \ { X } ) ) = ( R |` ( dom R \ { X } ) ) ) |