Description: The membership relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the membership relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | epse | |- _E Se A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | epel | |- ( y _E x <-> y e. x ) |
|
2 | 1 | bicomi | |- ( y e. x <-> y _E x ) |
3 | 2 | abbi2i | |- x = { y | y _E x } |
4 | vex | |- x e. _V |
|
5 | 3 4 | eqeltrri | |- { y | y _E x } e. _V |
6 | rabssab | |- { y e. A | y _E x } C_ { y | y _E x } |
|
7 | 5 6 | ssexi | |- { y e. A | y _E x } e. _V |
8 | 7 | rgenw | |- A. x e. A { y e. A | y _E x } e. _V |
9 | df-se | |- ( _E Se A <-> A. x e. A { y e. A | y _E x } e. _V ) |
|
10 | 8 9 | mpbir | |- _E Se A |