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

Metamath Proof Explorer

Theorem cnvepres

Description: Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018)

		Ref	Expression
	Assertion	cnvepres	$⊢ {E^{-1} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y \in x)\}$

Step	Hyp	Ref	Expression
1		dfres2	$⊢ {E^{-1} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land x E^{-1} y)\}$
2		brcnvep	$⊢ x \in V \to (x E^{-1} y \leftrightarrow y \in x)$
3	2	elv	$⊢ x E^{-1} y \leftrightarrow y \in x$
4	3	anbi2i	$⊢ (x \in A \land x E^{-1} y) \leftrightarrow (x \in A \land y \in x)$
5	4	opabbii	$⊢ \{⟨x, y⟩ \| (x \in A \land x E^{-1} y)\} = \{⟨x, y⟩ \| (x \in A \land y \in x)\}$
6	1 5	eqtri	$⊢ {E^{-1} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y \in x)\}$