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

Metamath Proof Explorer

Theorem rncnvepres

Description: The range of the restricted converse epsilon is the union of the restriction. (Contributed by Peter Mazsa, 11-Feb-2018) (Revised by Peter Mazsa, 26-Sep-2021)

		Ref	Expression
	Assertion	rncnvepres	$⊢ ran ({E^{-1} ↾}_{A}) = ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		rnopab	$⊢ ran \{⟨x, y⟩ \| (x \in A \land y \in x)\} = \{y \| \exists x (x \in A \land y \in x)\}$
2		cnvepres	$⊢ {E^{-1} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y \in x)\}$
3	2	rneqi	$⊢ ran ({E^{-1} ↾}_{A}) = ran \{⟨x, y⟩ \| (x \in A \land y \in x)\}$
4		dfuni2	$⊢ ⋃ A = \{y \| \exists x \in A y \in x\}$
5		df-rex	$⊢ \exists x \in A y \in x \leftrightarrow \exists x (x \in A \land y \in x)$
6	5	abbii	$⊢ \{y \| \exists x \in A y \in x\} = \{y \| \exists x (x \in A \land y \in x)\}$
7	4 6	eqtri	$⊢ ⋃ A = \{y \| \exists x (x \in A \land y \in x)\}$
8	1 3 7	3eqtr4i	$⊢ ran ({E^{-1} ↾}_{A}) = ⋃ A$