Step |
Hyp |
Ref |
Expression |
1 |
|
dffunsALTV |
|- FunsALTV = { f e. Rels | ,~ f e. CnvRefRels } |
2 |
|
cosselcnvrefrels3 |
|- ( ,~ f e. CnvRefRels <-> ( A. u A. x A. y ( ( u f x /\ u f y ) -> x = y ) /\ ,~ f e. Rels ) ) |
3 |
|
cosselrels |
|- ( f e. Rels -> ,~ f e. Rels ) |
4 |
3
|
biantrud |
|- ( f e. Rels -> ( A. u A. x A. y ( ( u f x /\ u f y ) -> x = y ) <-> ( A. u A. x A. y ( ( u f x /\ u f y ) -> x = y ) /\ ,~ f e. Rels ) ) ) |
5 |
2 4
|
bitr4id |
|- ( f e. Rels -> ( ,~ f e. CnvRefRels <-> A. u A. x A. y ( ( u f x /\ u f y ) -> x = y ) ) ) |
6 |
1 5
|
rabimbieq |
|- FunsALTV = { f e. Rels | A. u A. x A. y ( ( u f x /\ u f y ) -> x = y ) } |