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 e. V -> ( `' _E |` A ) e. _V )

Proof

Step Hyp Ref Expression
1 cnvepres
 |-  ( `' _E |` A ) = { <. x , y >. | ( x e. A /\ y e. x ) }
2 id
 |-  ( 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 )