Definition df-eprel 4995

Description: Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) when 𝐵 is a set by epelg 4996. Thus, 5 E {1, 5} (ex-eprel 27178). (Contributed by NM, 13-Aug-1995.)

Assertion

Ref	Expression
df-eprel	⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-eprel

Step	Hyp	Ref	Expression
1		cep 4993	. 2 class E
2		vx	. . . 4 setvar 𝑥
3		vy	. . . 4 setvar 𝑦
4	2, 3	wel 1988	. . 3 wff 𝑥 ∈ 𝑦
5	4, 2, 3	copab 4682	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
6	1, 5	wceq 1480	1 wff E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}

This definition is referenced by:  epelg  4996  rele  5220