This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \leftrightarrow y \in x$
2	1	bicomi	$⊢ y \in x \leftrightarrow y E x$
3	2	eqabi	$⊢ x = \{y \| y E x\}$
4		vex	$⊢ x \in V$
5	3 4	eqeltrri	$⊢ \{y \| y E x\} \in V$
6		rabssab	$⊢ \{y \in A \| y E x\} \subseteq \{y \| y E x\}$
7	5 6	ssexi	$⊢ \{y \in A \| y E x\} \in V$
8	7	rgenw	$⊢ \forall x \in A \{y \in A \| y E x\} \in V$
9		df-se	$⊢ E Se A \leftrightarrow \forall x \in A \{y \in A \| y E x\} \in V$
10	8 9	mpbir	$⊢ E Se A$