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

Metamath Proof Explorer

Theorem imacnvcnv

Description: The image of the double converse of a class. (Contributed by NM, 8-Apr-2007)

		Ref	Expression
	Assertion	imacnvcnv	$⊢ {A^{-1}}^{-1} [B] = A [B]$

Step	Hyp	Ref	Expression
1		rescnvcnv	$⊢ {{A^{-1}}^{-1} ↾}_{B} = {A ↾}_{B}$
2	1	rneqi	$⊢ ran ({{A^{-1}}^{-1} ↾}_{B}) = ran ({A ↾}_{B})$
3		df-ima	$⊢ {A^{-1}}^{-1} [B] = ran ({{A^{-1}}^{-1} ↾}_{B})$
4		df-ima	$⊢ A [B] = ran ({A ↾}_{B})$
5	2 3 4	3eqtr4i	$⊢ {A^{-1}}^{-1} [B] = A [B]$