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 𝐴

Proof

Step	Hyp	Ref	Expression
1		epel	⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
2	1	bicomi	⊢ ( 𝑦 ∈ 𝑥 ↔ 𝑦 E 𝑥 )
3	2	eqabi	⊢ 𝑥 = { 𝑦 ∣ 𝑦 E 𝑥 }
4		vex	⊢ 𝑥 ∈ V
5	3 4	eqeltrri	⊢ { 𝑦 ∣ 𝑦 E 𝑥 } ∈ V
6		rabssab	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 E 𝑥 } ⊆ { 𝑦 ∣ 𝑦 E 𝑥 }
7	5 6	ssexi	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 E 𝑥 } ∈ V
8	7	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 E 𝑥 } ∈ V
9		df-se	⊢ ( E Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 E 𝑥 } ∈ V )
10	8 9	mpbir	⊢ E Se 𝐴

Metamath Proof Explorer

Theorem epse

Proof