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 ) |
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 ) |