Theorem cnvcnv3

Description: The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015)

	Ref	Expression
Assertion	cnvcnv3	|- `' `' R = { <. x , y >. | x R y }

Proof

Step	Hyp	Ref	Expression
1		df-cnv	|- `' `' R = { <. x , y >. | y `' R x }
2		vex	|- y e. _V
3		vex	|- x e. _V
4	2 3	brcnv	|- ( y `' R x <-> x R y )
5	4	opabbii	|- { <. x , y >. | y `' R x } = { <. x , y >. | x R y }
6	1 5	eqtri	|- `' `' R = { <. x , y >. | x R y }