Step |
Hyp |
Ref |
Expression |
1 |
|
symrefref2 |
|- ( `' R C_ R -> ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I |` dom R ) C_ R ) ) |
2 |
|
cnvsym |
|- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) |
3 |
|
idinxpss |
|- ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> A. x e. dom R A. y e. ran R ( x = y -> x R y ) ) |
4 |
|
idrefALT |
|- ( ( _I |` dom R ) C_ R <-> A. x e. dom R x R x ) |
5 |
3 4
|
bibi12i |
|- ( ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I |` dom R ) C_ R ) <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) <-> A. x e. dom R x R x ) ) |
6 |
1 2 5
|
3imtr3i |
|- ( A. x A. y ( x R y -> y R x ) -> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) <-> A. x e. dom R x R x ) ) |