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	$$⊢\mathrm{E}\mathrm{Se}A$$

Proof

Step	Hyp	Ref	Expression
1		epel	$$⊢y\mathrm{E}x\leftrightarrow y\in x$$
2	1	bicomi	$$⊢y\in x\leftrightarrow y\mathrm{E}x$$
3	2	eqabi	$$⊢x=\left\{y|y\mathrm{E}x\right\}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	3 4	eqeltrri	$$⊢\left\{y|y\mathrm{E}x\right\}\in \mathrm{V}$$
6		rabssab	$$⊢\left\{y\in A|y\mathrm{E}x\right\}\subseteq \left\{y|y\mathrm{E}x\right\}$$
7	5 6	ssexi	$$⊢\left\{y\in A|y\mathrm{E}x\right\}\in \mathrm{V}$$
8	7	rgenw	$$⊢\forall x\in A\left\{y\in A|y\mathrm{E}x\right\}\in \mathrm{V}$$
9		df-se	$$⊢\mathrm{E}\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|y\mathrm{E}x\right\}\in \mathrm{V}$$
10	8 9	mpbir	$$⊢\mathrm{E}\mathrm{Se}A$$