Step |
Hyp |
Ref |
Expression |
1 |
|
df-refrel |
|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) ) |
2 |
|
dfrel6 |
|- ( Rel R <-> ( R i^i ( dom R X. ran R ) ) = R ) |
3 |
2
|
biimpi |
|- ( Rel R -> ( R i^i ( dom R X. ran R ) ) = R ) |
4 |
3
|
sseq2d |
|- ( Rel R -> ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) <-> ( _I i^i ( dom R X. ran R ) ) C_ R ) ) |
5 |
4
|
pm5.32ri |
|- ( ( ( _I i^i ( dom R X. ran R ) ) C_ ( R i^i ( dom R X. ran R ) ) /\ Rel R ) <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) ) |
6 |
1 5
|
bitri |
|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) ) |