Description: A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | relcnvexb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvexg | ||
2 | dfrel2 | ||
3 | cnvexg | ||
4 | eleq1 | ||
5 | 3 4 | imbitrid | |
6 | 2 5 | sylbi | |
7 | 1 6 | impbid2 |