Step |
Hyp |
Ref |
Expression |
1 |
|
cosselcnvrefrels2 |
|- ( ,~ R e. CnvRefRels <-> ( ,~ R C_ _I /\ ,~ R e. Rels ) ) |
2 |
|
cossssid5 |
|- ( ,~ R C_ _I <-> A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) ) |
3 |
2
|
anbi1i |
|- ( ( ,~ R C_ _I /\ ,~ R e. Rels ) <-> ( A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) /\ ,~ R e. Rels ) ) |
4 |
1 3
|
bitri |
|- ( ,~ R e. CnvRefRels <-> ( A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) /\ ,~ R e. Rels ) ) |