Theorem relcnvexb

Description: A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007)

	Ref	Expression
Assertion	relcnvexb	|- ( Rel R -> ( R e. _V <-> `' R e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		cnvexg	|- ( R e. _V -> `' R e. _V )
2		dfrel2	|- ( Rel R <-> `' `' R = R )
3		cnvexg	|- ( `' R e. _V -> `' `' R e. _V )
4		eleq1	|- ( `' `' R = R -> ( `' `' R e. _V <-> R e. _V ) )
5	3 4	syl5ib	|- ( `' `' R = R -> ( `' R e. _V -> R e. _V ) )
6	2 5	sylbi	|- ( Rel R -> ( `' R e. _V -> R e. _V ) )
7	1 6	impbid2	|- ( Rel R -> ( R e. _V <-> `' R e. _V ) )