Definition df-eprel 5177

Description: Define the membership relation, or 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 5178. Thus, 5 E {1, 5} (ex-eprel 27599). (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 5176	. 2 class E
2		vx	. . . 4 setvar 𝑥
3		vy	. . . 4 setvar 𝑦
4	2, 3	wel 2138	. . 3 wff 𝑥 ∈ 𝑦
5	4, 2, 3	copab 4862	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
6	1, 5	wceq 1630	1 wff E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}

This definition is referenced by:  epelg  5178  rele  5404  epinid0  8668  cnvepnep  8674  dfnelbr2  41797