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