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

Metamath Proof Explorer

Theorem cnvi

Description: The converse of the identity relation. Theorem 3.7(ii) of Monk1 p. 36. (Contributed by NM, 26-Apr-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	cnvi	$⊢ I^{-1} = I$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	ideq	$⊢ y I x \leftrightarrow y = x$
3		equcom	$⊢ y = x \leftrightarrow x = y$
4	2 3	bitri	$⊢ y I x \leftrightarrow x = y$
5	4	opabbii	$⊢ \{⟨x, y⟩ \| y I x\} = \{⟨x, y⟩ \| x = y\}$
6		df-cnv	$⊢ I^{-1} = \{⟨x, y⟩ \| y I x\}$
7		df-id	$⊢ I = \{⟨x, y⟩ \| x = y\}$
8	5 6 7	3eqtr4i	$⊢ I^{-1} = I$