rnxrncnvepres

Description: Range of a range Cartesian product with a restriction of the converse epsilon relation. (Contributed by Peter Mazsa, 6-Dec-2021)

		Ref	Expression
	Assertion	rnxrncnvepres	$⊢ ran R ⋉ ({E^{-1} ↾}_{A}) = \{⟨x, y⟩ \| \exists u \in A (y \in u \land u R x)\}$

Step	Hyp	Ref	Expression
1		rnxrnres	$⊢ ran R ⋉ ({E^{-1} ↾}_{A}) = \{⟨x, y⟩ \| \exists u \in A (u R x \land u E^{-1} y)\}$
2		brcnvep	$⊢ u \in V \to (u E^{-1} y \leftrightarrow y \in u)$
3	2	elv	$⊢ u E^{-1} y \leftrightarrow y \in u$
4	3	anbi1ci	$⊢ (u R x \land u E^{-1} y) \leftrightarrow (y \in u \land u R x)$
5	4	rexbii	$⊢ \exists u \in A (u R x \land u E^{-1} y) \leftrightarrow \exists u \in A (y \in u \land u R x)$
6	5	opabbii	$⊢ \{⟨x, y⟩ \| \exists u \in A (u R x \land u E^{-1} y)\} = \{⟨x, y⟩ \| \exists u \in A (y \in u \land u R x)\}$
7	1 6	eqtri	$⊢ ran R ⋉ ({E^{-1} ↾}_{A}) = \{⟨x, y⟩ \| \exists u \in A (y \in u \land u R x)\}$

Metamath Proof Explorer