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

Metamath Proof Explorer

Theorem cnvepresex

Description: Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018)

		Ref	Expression
	Assertion	cnvepresex	$⊢ A \in V \to {E^{-1} ↾}_{A} \in V$

Step	Hyp	Ref	Expression
1		cnvepres	$⊢ {E^{-1} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y \in x)\}$
2		id	$⊢ A \in V \to A \in V$
3		abid2	$⊢ \{y \| y \in x\} = x$
4		vex	$⊢ x \in V$
5	3 4	eqeltri	$⊢ \{y \| y \in x\} \in V$
6	5	a1i	$⊢ (A \in V \land x \in A) \to \{y \| y \in x\} \in V$
7	2 6	opabex3d	$⊢ A \in V \to \{⟨x, y⟩ \| (x \in A \land y \in x)\} \in V$
8	1 7	eqeltrid	$⊢ A \in V \to {E^{-1} ↾}_{A} \in V$