This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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^{-1}}^{-1} = \{⟨x, y⟩ \| x R y\}$

Step	Hyp	Ref	Expression
1		df-cnv	$⊢ {R^{-1}}^{-1} = \{⟨x, y⟩ \| y R^{-1} x\}$
2		vex	$⊢ y \in V$
3		vex	$⊢ x \in V$
4	2 3	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
5	4	opabbii	$⊢ \{⟨x, y⟩ \| y R^{-1} x\} = \{⟨x, y⟩ \| x R y\}$
6	1 5	eqtri	$⊢ {R^{-1}}^{-1} = \{⟨x, y⟩ \| x R y\}$