Metamath Proof Explorer


Theorem epse

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

Proof

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