Theorem cnvepresex

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

	Ref	Expression
Assertion	cnvepresex	|- ( A e. V -> ( `' _E |` A ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		cnvepres	|- ( `' _E |` A ) = { <. x , y >. | ( x e. A /\ y e. x ) }
2		elex	|- ( A e. V -> A e. _V )
3		abid2	|- { y | y e. x } = x
4		vex	|- x e. _V
5	3 4	eqeltri	|- { y | y e. x } e. _V
6	5	a1i	|- ( ( A e. V /\ x e. A ) -> { y | y e. x } e. _V )
7	2 6	opabex3d	|- ( A e. V -> { <. x , y >. | ( x e. A /\ y e. x ) } e. _V )
8	1 7	eqeltrid	|- ( A e. V -> ( `' _E |` A ) e. _V )